90 const auto size_of_expr_opt =
size_of_expr(dereference_type, ns);
143 const exprt &pointer,
150 const exprt &pointer,
152 const exprt &access_size)
163 exprt sum=object_offset;
179 const exprt &pointer,
180 const exprt &access_size)
191 exprt sum=object_offset;
209 const exprt &pointer,
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_size_type()
A base class for relations, i.e., binary predicates whose two operands have the same type.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
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.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt malloc_object(const exprt &pointer, const namespacet &ns)
exprt dynamic_size(const namespacet &ns)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt good_pointer(const exprt &pointer)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt dynamic_object(const exprt &pointer)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
exprt null_object(const exprt &pointer)
exprt null_pointer(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.
#define CHECK_RETURN(CONDITION)
API to expression classes.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.