23 std::vector<path_symex_step_reft> steps;
28 for(step_nr=0; step_nr<steps.size(); step_nr++)
35 trace_step.
pc=state.
locs[step.
pc].target;
39 const goto_programt::instructiont &instruction=*trace_step.
pc;
41 switch(instruction.type)
92 const goto_programt::instructiont &instruction=
95 assert(instruction.is_assert());
106 instruction.source_location.get_comment();
111 trace_step.
comment=
"assertion";
const std::string & id2string(const irep_idt &d)
void build_history(std::vector< path_symex_step_reft > &dest) const
std::string comment(const rw_set_baset::entryt &entry, bool write)
virtual exprt get(const exprt &expr) const =0
goto_programt::const_targett pc
void add_step(const goto_trace_stept &step)
Build Goto Trace from Path Symex History.
unsigned get_current_thread() const
goto_programt::const_targett get_instruction() const
Expression providing an SSA-renamed symbol of expressions.
path_symex_step_reft history
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)