cprover
|
Traces of GOTO Programs. More...
Go to the source code of this file.
Typedefs | |
typedef std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> | ssa_step_predicatet |
Functions | |
void | build_goto_trace (const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace) |
void | build_goto_trace (const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace) |
void | build_goto_trace (const symex_target_equationt &target, ssa_step_predicatet stop_after_predicate, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace) |
Traces of GOTO Programs.
Definition in file build_goto_trace.h.
typedef std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet |
Definition at line 37 of file build_goto_trace.h.
void build_goto_trace | ( | const symex_target_equationt & | target, |
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 389 of file build_goto_trace.cpp.
void build_goto_trace | ( | const symex_target_equationt & | target, |
symex_target_equationt::SSA_stepst::const_iterator | last_step_to_keep, | ||
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
void build_goto_trace | ( | const symex_target_equationt & | target, |
ssa_step_predicatet | stop_after_predicate, | ||
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 166 of file build_goto_trace.cpp.