const code_deadt & get_dead() const
Get the dead statement for DEAD.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
goto_programt::const_targett pc
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.
Central data structure: state.
void erase_if_exists(const key_type &k)
Erase element if it exists.
Base class for all expressions.
symex_targett::sourcet source
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
Expression to hold a symbol (variable)
sharing_mapt< irep_idt, exprt > propagation
Expression providing an SSA-renamed symbol of expressions.
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
A codet representing the removal of a local variable going out of scope.
field_sensitivityt field_sensitivity
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
std::unordered_set< irep_idt > find_symbols_sett
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
valuest values
Stores the LHS ID -> RHS expression set map.