57 for(symex_target_equationt::SSA_stepst::const_iterator
73 if(expr.
id()==ID_symbol)
77 else if(expr.
id()==ID_index)
82 else if(expr.
id()==ID_member)
86 else if(expr.
id()==ID_dereference)
105 if(dest.
id()==ID_and &&
119 if(
is_used(dest, lhs_identifier))
150 if(expr.
id()==ID_address_of)
154 else if(expr.
id()==ID_symbol &&
159 else if(expr.
id()==ID_symbol)
163 else if(expr.
id()==ID_dereference)
168 std::unordered_set<irep_idt> symbols;
170 for(value_setst::valuest::const_iterator
180 return symbols.find(identifier)!=symbols.end();
const irep_idt & get_identifier() const
bool is_false() const
Return whether the expression is a constant representing false.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
void compute(exprt &dest)
bool get_bool(const irep_namet &name) const
const value_sett & value_set
postconditiont(const namespacet &_ns, const value_sett &_value_set, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void get_original_name(exprt &expr) const
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
The Boolean constant true.
Generate Equation using Symbolic Execution.
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
State type in value_set_domaint, used in value-set analysis and goto-symex.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
void strengthen(exprt &dest)
Single SSA step in the equation.
Base class for all expressions.
irep_idt get_object_name() const
#define Forall_operands(it, expr)
bool is_used(const exprt &expr, const irep_idt &identifier)
const goto_symex_statet & s
std::list< exprt > valuest
const symex_target_equationt::SSA_stept & SSA_step
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
void find_symbols(const exprt &src, find_symbols_sett &dest)