23 const goto_programt::instructiont &instruction=*state.
source.
pc;
26 exprt old_guard=instruction.guard;
29 exprt new_guard=old_guard;
46 assert(!instruction.targets.empty());
49 if(instruction.targets.size()!=1)
50 throw "no support for non-deterministic gotos";
53 instruction.get_target();
55 bool forward=!instruction.is_backwards_goto();
61 (instruction.incoming_edges.size()==1 &&
62 *instruction.incoming_edges.begin()==goto_target))
107 new_state_pc=goto_target;
113 while(state_pc!=goto_target && !state_pc->is_target())
116 if(state_pc==goto_target)
126 state_pc=goto_target;
148 if(new_guard.
id()==ID_symbol ||
149 (new_guard.
id()==ID_not &&
151 new_guard.
op0().
id()==ID_symbol))
152 guard_expr=new_guard;
157 exprt new_rhs=new_guard;
168 new_lhs, new_lhs, guard_symbol_expr,
173 guard_expr=guard_symbol_expr;
195 const goto_programt::instructiont &instruction=*state.
source.
pc;
197 exprt guard(instruction.guard);
215 statet::goto_state_mapt::iterator state_map_it=
224 for(statet::goto_state_listt::reverse_iterator
225 list_it=state_list.rbegin();
226 list_it!=state_list.rend();
240 throw "atomic sections differ across branches";
272 std::unordered_set<ssa_exprt, irep_hash> variables;
279 if(!variables.empty())
281 diff_guard=goto_state.
guard;
284 diff_guard-=dest_state.
guard;
287 for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
288 it=variables.begin();
292 const irep_idt l1_identifier=it->get_identifier();
293 const irep_idt &obj_identifier=it->get_object_name();
310 dest_state.
threads.size()>=2 &&
318 if(!it->get_level_0().empty() &&
322 exprt goto_state_rhs=*it, dest_state_rhs=*it;
325 goto_symex_statet::propagationt::valuest::const_iterator p_it=
329 goto_state_rhs=p_it->second;
336 goto_symex_statet::propagationt::valuest::const_iterator p_it=
340 dest_state_rhs=p_it->second;
377 const unsigned loop_number=state.
source.
pc->loop_number;
386 bool unwinding_assertions=
394 if(unwinding_assertions)
398 "unwinding assertion loop "+std::to_string(loop_number),
virtual void do_simplify(exprt &expr)
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
virtual void symex_step_goto(statet &state, bool taken)
irep_idt guard_identifier
static irep_idt loop_id(const_targett target)
Human-readable loop name.
virtual void location(const exprt &guard, const sourcet &source)=0
goto_programt::const_targett pc
virtual void symex_assume(statet &state, const exprt &cond)
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 merge_goto(const statet::goto_statet &goto_state, statet &state)
Variables whose address is taken.
virtual void dereference(exprt &expr, statet &state, const bool write)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool make_union(object_mapt &dest, const object_mapt &src) const
The trinary if-then-else operator.
loop_iterationst loop_iterations
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...
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
unsigned level2_current_count(const irep_idt &identifier) const
goto_symex_statet::level2t level2
const irep_idt & id() const
unsigned atomic_section_id
instructionst::const_iterator const_targett
The boolean constant true.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
API to expression classes.
bool get_bool_option(const std::string &option) const
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
goto_state_mapt goto_state_map
void clean_expr(exprt &expr, statet &state, bool write)
unsigned atomic_section_id
void merge_gotos(statet &state)
The boolean constant false.
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)=0
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
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)=0
virtual void symex_goto(statet &state)
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
const exprt & get_original_expr() const
void phi_function(const statet::goto_statet &goto_state, statet &state)
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Expression to hold a symbol (variable)
std::list< goto_statet > goto_state_listt
Expression providing an SSA-renamed symbol of expressions.
void add(const exprt &expr)
symex_targett::sourcet source