CBMC
|
Traces of GOTO Programs. More...
#include "symex_target_equation.h"
Go to the source code of this file.
Typedefs | |
typedef std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> | ssa_step_predicatet |
Functions | |
void | build_goto_trace (const symex_target_equationt &target, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) |
Build a trace by going through the steps of target and stopping at the first failing assertion. More... | |
void | build_goto_trace (const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) |
Build a trace by going through the steps of target and stopping after the given step. More... | |
void | build_goto_trace (const symex_target_equationt &target, ssa_step_predicatet stop_after_predicate, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) |
Build a trace by going through the steps of target and stopping after the step matching a given condition. More... | |
Traces of GOTO Programs.
Definition in file build_goto_trace.h.
typedef std::function<bool( symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet |
Definition at line 48 of file build_goto_trace.h.
void build_goto_trace | ( | const symex_target_equationt & | target, |
const decision_proceduret & | decision_procedure, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Build a trace by going through the steps of target
and stopping at the first failing assertion.
target | SSA form of the program | |
decision_procedure | solver from which to get valuations | |
ns | namespace | |
[out] | goto_trace | trace to which the steps of the trace get appended |
Definition at line 452 of file build_goto_trace.cpp.
void build_goto_trace | ( | const symex_target_equationt & | target, |
ssa_step_predicatet | stop_after_predicate, | ||
const decision_proceduret & | decision_procedure, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Build a trace by going through the steps of target
and stopping after the step matching a given condition.
target | SSA form of the program | |
stop_after_predicate | function with an SSA step iterator and solver as argument, which should return true for the last step to keep | |
decision_procedure | solver from which to get valuations | |
ns | namespace | |
[out] | goto_trace | trace to which the steps of the trace get appended |
Definition at line 207 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 decision_proceduret & | decision_procedure, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Build a trace by going through the steps of target
and stopping after the given step.
target | SSA form of the program | |
last_step_to_keep | iterator pointing to the last step to keep | |
decision_procedure | solver from which to get valuations | |
ns | namespace | |
[out] | goto_trace | trace to which the steps of the trace get appended |
Definition at line 428 of file build_goto_trace.cpp.