32 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
The Boolean constant false.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The Boolean constant true.
bool stack_and_not_dirty(const exprt &expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt strip_member_element(const exprt &src)
exprt may_be_same_object(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
API to expression classes for Pointers.
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Various predicates over pointers in programs.