59 for(symex_target_equationt::SSA_stepst::const_iterator
75 if(expr.
id()==ID_symbol)
79 else if(expr.
id()==ID_index)
84 else if(expr.
id()==ID_member)
88 else if(expr.
id()==ID_dereference)
107 if(dest.
id()==ID_and &&
121 if(
is_used(dest, lhs_identifier))
152 if(expr.
id()==ID_address_of)
160 else if(expr.
id()==ID_symbol)
164 else if(expr.
id()==ID_dereference)
167 const std::vector<exprt> expr_set =
169 const auto original_names =
make_range(expr_set).map(
171 const std::unordered_set<irep_idt> symbols =
173 return symbols.find(identifier)!=symbols.end();
Single SSA step in the equation.
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_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
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 SSA_stept & SSA_step
bool is_used(const exprt &expr, const irep_idt &identifier)
void strengthen(exprt &dest)
const value_sett & value_set
const goto_symex_statet & s
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
postconditiont(const namespacet &_ns, const value_sett &_value_set, const SSA_stept &_SSA_step, const goto_symex_statet &_s)
void compute(exprt &dest)
irep_idt get_object_name() const
const irep_idt & get_identifier() const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The Boolean constant true.
State type in value_set_domaint, used in value-set analysis and goto-symex.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
#define forall_operands(it, expr)
#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.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
Generate Equation using Symbolic Execution.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt get_original_name(exprt expr)
Undo all levels of renaming.
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Generate Equation using Symbolic Execution.