56 for(
const auto &op :
l1_expr.operands())
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr, bool disjoined_fields_only) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
sharing_mapt< irep_idt, exprt > propagation
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Central data structure: state.
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
field_sensitivityt field_sensitivity
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
symex_targett::sourcet source
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::vector< threadt > threads
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void erase_if_exists(const key_type &k)
Erase element if it exists.
Expression providing an SSA-renamed symbol of expressions.
Expression to hold a symbol (variable)
valuest values
Stores the LHS ID -> RHS expression set map.
#define UNREACHABLE
This should be used to mark dead code.
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.
goto_programt::const_targett pc
static void remove_l1_object_rec(goto_symext::statet &state, const exprt &l1_expr, const namespacet &ns)