74 const exprt &access_size)
80 std::size_t max_width = std::max(
118 const exprt &pointer,
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
Base class for all expressions.
typet & type()
Return the type of the expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
Fixed-width bit-vector with unsigned binary interpretation.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
exprt pointer_object(const exprt &p)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
API to expression classes.