Go to the documentation of this file.
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,
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
exprt pointer_object(const exprt &p)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
exprt null_pointer(const exprt &pointer)
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Various predicates over pointers in programs.
The plus expression Associativity is not specified.
Base class for all expressions.
Generic base class for unary expressions.
exprt good_pointer(const exprt &pointer)
exprt dynamic_object(const exprt &pointer)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
exprt deallocated(const exprt &pointer, const namespacet &ns)
signedbv_typet signed_size_type()
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt integer_address(const exprt &pointer)
pointer_typet pointer_type(const typet &subtype)
exprt object_size(const exprt &pointer)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
exprt pointer_offset(const exprt &pointer)
exprt null_object(const exprt &pointer)
exprt malloc_object(const exprt &pointer, const namespacet &ns)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
A base class for relations, i.e., binary predicates whose two operands have the same type.
exprt same_object(const exprt &p1, const exprt &p2)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
unsignedbv_typet size_type()
API to expression classes.
exprt dynamic_size(const namespacet &ns)