12 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H 13 #define CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H 163 void output(std::ostream &out)
const;
164 void output(
const threadt &thread, std::ostream &out)
const;
169 return read(src,
true);
175 return read(src,
false);
247 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
History for path-based symbolic simulator.
var_state_mapt saved_local_vars
exprt instantiate_rec(const exprt &src, bool propagate)
std::map< loc_reft, unsigned > unwinding_mapt
bool inside_atomic_section
void disable_current_thread()
std::set< exprt > index_sett
exprt read_no_propagate(const exprt &src)
exprt instantiate_rec_address(const exprt &src, bool propagate)
unwinding_mapt unwinding_map
exprt array_theory(const exprt &src, bool propagate)
bool last_was_branch() const
std::string array_index_as_string(const exprt &) const
unsigned no_thread_interleavings
instructionst::const_iterator const_targett
exprt read(const exprt &src)
std::map< unsigned, var_statet > var_state_mapt
std::vector< var_statet > var_valt
path_symex_statet(var_mapt &_var_map, const locst &_locs, path_symex_historyt &_path_symex_history)
#define PRECONDITION(CONDITION)
bool is_feasible(class decision_proceduret &) const
var_statet & get_var_state(const var_mapt::var_infot &var_info)
unsigned get_current_thread() const
irep_idt current_function
unsigned get_no_thread_interleavings() const
exprt dereference_rec(const exprt &src, bool propagate)
exprt read_symbol_member_index(const exprt &src, bool propagate)
exprt expand_structs_and_arrays(const exprt &src)
std::map< irep_idt, unsigned > recursion_mapt
bool check_assertion(class decision_proceduret &)
recursion_mapt recursion_map
goto_programt::const_targett get_instruction() const
std::vector< framet > call_stackt
Base class for all expressions.
bool is_executable() const
void set_pc(loc_reft new_pc)
unsigned get_no_branches() const
CFG made of Program Locations, built from goto_functionst.
Expression to hold a symbol (variable)
bool is_symbol_member_index(const exprt &src) const
void set_current_thread(unsigned _thread)
path_symex_step_reft history
std::vector< threadt > threadst
void output(std::ostream &out) const
path_symex_statet initial_state(var_mapt &var_map, const locst &locs, path_symex_historyt &)
unsigned get_depth() const