25 const goto_programt::instructiont &instruction=*state.
source.
pc;
30 throw "two-operand decl not supported here";
33 throw "decl expects one operand";
35 if(code.
op0().
id()!=ID_symbol)
36 throw "decl expects symbol as first operand";
65 address_of_expr.
object()=failed;
70 rhs=
exprt(ID_invalid);
96 state.
source.
pc->source_location.get_hide();
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
goto_programt::const_targett pc
class goto_symex_statet::propagationt propagation
Variables whose address is taken.
void remove(const irep_idt &identifier)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_decl(statet &state)
const irep_idt & get_identifier() const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
void increase_counter(const irep_idt &identifier)
goto_symex_statet::level2t level2
const irep_idt & id() const
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
API to expression classes.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
current_namest current_names
Operator to return the address of an object.
unsigned atomic_section_id
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt get_object_name() const
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
A statement in a programming language.
Expression providing an SSA-renamed symbol of expressions.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
symex_targett::sourcet source