62 for(symex_target_equationt::SSA_stepst::const_reverse_iterator
76 if(dest.
id()==ID_symbol)
80 else if(dest.
id()==ID_index)
86 else if(dest.
id()==ID_member)
90 else if(dest.
id()==ID_dereference)
103 if(dest.
id()==ID_address_of)
108 else if(dest.
id()==ID_dereference)
118 const std::unordered_set<irep_idt> symbols =
121 if(symbols.find(lhs_identifier)!=symbols.end())
125 tmp.
swap(deref_expr.pointer());
127 deref_expr.swap(tmp);
Single SSA step in the equation.
symex_targett::sourcet source
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_false() const
Return whether the expression is a constant representing false.
instructionst::const_iterator const_targett
Central data structure: state.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const goto_programt::const_targett target
void compute_address_of(exprt &dest)
void compute_rec(exprt &dest)
const SSA_stept & SSA_step
preconditiont(const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const SSA_stept &_SSA_step, const goto_symex_statet &_s)
const goto_symex_statet & s
void compute(exprt &dest)
const exprt & get_original_expr() const
irep_idt get_object_name() const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
#define Forall_operands(it, expr)
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void precondition(const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
Generate Equation using Symbolic Execution.
exprt get_original_name(exprt expr)
Undo all levels of renaming.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Generate Equation using Symbolic Execution.