42 rhs=
exprt(ID_invalid);
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
goto_programt::const_targett pc
const code_deadt & to_code_dead(const codet &code)
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...
typet & type()
Return the type of the expression.
std::map< irep_idt, exprt > propagation
This class represents an instruction in the GOTO intermediate representation.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
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 an exprt to a symbol_exprt.
current_namest current_names
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
Base class for all expressions.
virtual void symex_dead(statet &)
A codet representing the removal of a local variable going out of scope.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Expression providing an SSA-renamed symbol of expressions.
symex_targett::sourcet source