30 exprt new_guard=old_guard;
48 !instruction.
targets.empty(),
"goto should have at least one target");
51 if(instruction.
targets.size()!=1)
52 throw "no support for non-deterministic gotos";
114 (simpl_state_guard.
is_true() ||
120 instruction.
targets.size() > 0,
121 "Instruction is an unconditional goto with no target: " +
132 new_state_pc=goto_target;
138 while(state_pc!=goto_target && !state_pc->is_target())
141 if(state_pc==goto_target)
151 state_pc=goto_target;
162 "Tried to explore the other path of a branch, but the next " 163 "instruction along that path is not the same as the instruction " 164 "that we saved at the branch point. Saved instruction is " +
166 "\nwe were intending " 168 new_state_pc->code.pretty() +
170 "instruction we think we saw on a previous path exploration is " +
171 state_pc->code.pretty());
173 new_state_pc = state_pc;
181 log.
debug() <<
"Resuming from next instruction '" 202 log.
debug() <<
"Saving next instruction '" 205 log.
debug() <<
"Saving jump target '" 235 if(new_guard.
id()==ID_symbol ||
236 (new_guard.
id()==ID_not &&
238 new_guard.
op0().
id()==ID_symbol))
239 guard_expr=new_guard;
244 exprt new_rhs=new_guard;
263 new_lhs, new_lhs, guard_symbol_expr,
268 guard_expr=guard_symbol_expr;
324 statet::goto_state_mapt::iterator state_map_it=
333 for(statet::goto_state_listt::reverse_iterator
334 list_it=state_list.rbegin();
335 list_it!=state_list.rend();
349 throw "atomic sections differ across branches";
381 std::unordered_set<ssa_exprt, irep_hash> variables;
388 if(!variables.empty())
390 diff_guard=goto_state.
guard;
393 diff_guard-=dest_state.
guard;
396 for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
397 it=variables.begin();
401 const irep_idt l1_identifier=it->get_identifier();
402 const irep_idt &obj_identifier=it->get_object_name();
427 if(!it->get_level_0().empty() &&
431 exprt goto_state_rhs=*it, dest_state_rhs=*it;
434 goto_symex_statet::propagationt::valuest::const_iterator p_it=
438 goto_state_rhs=p_it->second;
445 goto_symex_statet::propagationt::valuest::const_iterator p_it=
449 dest_state_rhs=p_it->second;
467 rhs = dest_state_rhs;
471 rhs = goto_state_rhs;
506 const unsigned loop_number=state.
source.
pc->loop_number;
515 bool unwinding_assertions=
523 if(unwinding_assertions)
exprt guard
Guard for gotos, assume, assert.
irep_idt name
The unique identifier.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
irep_idt guard_identifier
goto_programt::const_targett pc
void guard_expr(exprt &dest) const
void level2_get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
class goto_symex_statet::propagationt propagation
virtual void symex_goto(statet &)
std::set< targett > incoming_edges
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Variables whose address is taken.
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
record a goto instruction
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
virtual void symex_step_goto(statet &, bool taken)
The trinary if-then-else operator.
loop_iterationst loop_iterations
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
void set_level_2(unsigned i)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual void do_simplify(exprt &)
static mstreamt & eom(mstreamt &m)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
#define INVARIANT(CONDITION, REASON)
unsigned level2_current_count(const irep_idt &identifier) const
targetst targets
The list of successor instructions.
unsigned depth
distance from entry
This class represents an instruction in the GOTO intermediate representation.
virtual void dereference(exprt &, statet &, const bool write)
goto_symex_statet::level2t level2
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
bool self_loops_to_assumptions
const irep_idt & id() const
unsigned atomic_section_id
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
The boolean constant true.
source_locationt source_location
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
virtual void symex_assume(statet &, const exprt &cond)
API to expression classes.
bool get_bool_option(const std::string &option) const
symex_target_equationt & target
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
instructionst::const_iterator const_targett
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
write to a variable
path_storaget & path_storage
goto_state_mapt goto_state_map
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
unsigned atomic_section_id
virtual void loop_bound_exceeded(statet &, const exprt &guard)
The boolean constant false.
void phi_function(const statet::goto_statet &goto_state, statet &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
bool saved_target_is_backwards
void clean_expr(exprt &, statet &, bool write)
unsigned current_count(const irep_idt &identifier) const
goto_programt::const_targett saved_target
bool should_pause_symex
Have states been pushed onto the workqueue?
Base class for all expressions.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const exprt & get_original_expr() const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to mstream using output_generator if the configured verbosity is at least as high as ...
virtual void location(const exprt &guard, const sourcet &source)
just record a location
Information saved at a conditional goto to resume execution.
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
Expression to hold a symbol (variable)
#define DATA_INVARIANT(CONDITION, REASON)
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
std::list< goto_statet > goto_state_listt
const bool doing_path_exploration
Expression providing an SSA-renamed symbol of expressions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void add(const exprt &expr)
symex_targett::sourcet source