14 #ifndef CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H 15 #define CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H 30 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
35 typedef std::function<
36 bool(symex_target_equationt::SSA_stepst::const_iterator,
const prop_convt &)>
47 #endif // CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H Generate Equation using Symbolic Execution.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet
void build_goto_trace(const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...