27 throw "dead expects one operand";
29 if(code.
op0().
id()!=ID_symbol)
30 throw "dead expects symbol as first operand";
49 rhs=
exprt(ID_invalid);
goto_programt::const_targett pc
class goto_symex_statet::propagationt propagation
void remove(const irep_idt &identifier)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it...
void increase_counter(const irep_idt &identifier)
This class represents an instruction in the GOTO intermediate representation.
goto_symex_statet::level2t level2
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
current_namest current_names
Operator to return the address of an object.
Base class for all expressions.
virtual void symex_dead(statet &)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
A statement in a programming language.
Expression providing an SSA-renamed symbol of expressions.
symex_targett::sourcet source