cprover
build_goto_trace.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Traces of GOTO Programs
4
5
Author: Daniel Kroening
6
7
Date: July 2005
8
9
\*******************************************************************/
10
13
14
#ifndef CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
15
#define CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
16
17
#include "
symex_target_equation.h
"
18
#include "
goto_symex_state.h
"
19
20
// builds a trace that stops at first failing assertion
21
void
build_goto_trace
(
22
const
symex_target_equationt
&target,
23
const
prop_convt
&prop_conv,
24
const
namespacet
&ns,
25
goto_tracet
&goto_trace);
26
27
// builds a trace that stops after the given step
28
void
build_goto_trace
(
29
const
symex_target_equationt
&target,
30
symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
31
const
prop_convt
&prop_conv,
32
const
namespacet
&ns,
33
goto_tracet
&goto_trace);
34
35
typedef
std::function<
36
bool(symex_target_equationt::SSA_stepst::const_iterator,
const
prop_convt
&)>
37
ssa_step_predicatet
;
38
39
// builds a trace that stops after the step matching a given condition
40
void
build_goto_trace
(
41
const
symex_target_equationt
&target,
42
ssa_step_predicatet
stop_after_predicate,
43
const
prop_convt
&prop_conv,
44
const
namespacet
&ns,
45
goto_tracet
&goto_trace);
46
47
#endif // CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
symex_target_equation.h
prop_convt
Definition:
prop_conv.h:27
ssa_step_predicatet
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet
Definition:
build_goto_trace.h:37
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition:
symex_target_equation.h:35
goto_symex_state.h
goto_tracet
TO_BE_DOCUMENTED.
Definition:
goto_trace.h:150
build_goto_trace
void build_goto_trace(const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
Definition:
build_goto_trace.cpp:389
goto-symex
build_goto_trace.h
Generated by
1.8.17