46 out <<
" PC: " << thread.
pc <<
'\n';
47 out <<
" Call stack:";
48 for(call_stackt::const_iterator
52 out <<
" " << it->return_location <<
'\n';
58 for(
unsigned t=0; t<
threads.size(); t++)
60 out <<
"*** Thread " << t <<
'\n';
73 if(var_val.size()<=var_info.
number)
74 var_val.resize(var_info.
number+1);
75 return var_val[var_info.
number];
108 switch(decision_procedure())
115 throw "error from decision procedure";
127 assert(instruction.is_assert());
133 if(assertion.is_true())
140 decision_procedure.
set_to(assertion,
false);
152 throw "error from decision procedure";
Decision Procedure Interface.
unsigned no_thread_interleavings
virtual resultt dec_solve()=0
exprt read(const exprt &src)
void generate_successor()
std::vector< var_statet > var_valt
bool is_feasible(class decision_proceduret &) const
var_statet & get_var_state(const var_mapt::var_infot &var_info)
virtual void set_to(const exprt &expr, bool value)=0
bool check_assertion(class decision_proceduret &)
goto_programt::const_targett get_instruction() const
State of path-based symbolic simulator.
Base class for all expressions.
path_symex_statet initial_state(var_mapt &var_map, const locst &locs, path_symex_historyt &path_symex_history)
void set_current_thread(unsigned _thread)
path_symex_step_reft history
void output(std::ostream &out) const