Go to the documentation of this file.
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();
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define Forall_operands(it, expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
void get_original_name(exprt &expr) const
Single SSA step in the equation.
State type in value_set_domaint, used in value-set analysis and goto-symex.
Base class for all expressions.
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
irep_idt get_object_name() const
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.
void strengthen(exprt &dest)
bool is_false() const
Return whether the expression is a constant representing false.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::list< exprt > valuest
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define forall_operands(it, expr)
const irep_idt & get_identifier() const
const goto_symex_statet & s
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void compute(exprt &dest)
const irep_idt & id() const
bool is_used(const exprt &expr, const irep_idt &identifier)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const value_sett & value_set
const symex_target_equationt::SSA_stept & SSA_step
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
postconditiont(const namespacet &_ns, const value_sett &_value_set, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s)
The Boolean constant true.