61 for(symex_target_equationt::SSA_stepst::const_reverse_iterator
75 if(dest.
id()==ID_symbol)
79 else if(dest.
id()==ID_index)
85 else if(dest.
id()==ID_member)
90 else if(dest.
id()==ID_dereference)
104 if(dest.
id()==ID_address_of)
110 else if(dest.
id()==ID_dereference)
120 std::unordered_set<irep_idt> symbols;
122 for(value_setst::valuest::const_iterator
128 if(symbols.find(lhs_identifier)!=symbols.end())
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)
virtual void get_values(goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
preconditiont(const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s)
const symex_target_equationt::SSA_stept & SSA_step
void compute_rec(exprt &dest)
void get_original_name(exprt &expr) const
const irep_idt & id() const
exprt dereference(const exprt &pointer, const namespacet &ns)
void compute(exprt &dest)
instructionst::const_iterator const_targett
const goto_programt::const_targett target
const goto_symex_statet & s
void compute_address_of(exprt &dest)
Base class for all expressions.
irep_idt get_object_name() const
const exprt & get_original_expr() const
#define Forall_operands(it, expr)
std::list< exprt > valuest
void find_symbols(const exprt &src, find_symbols_sett &dest)
Generate Equation using Symbolic Execution.