147 const exprt &pointer,
155 const exprt &pointer,
157 const exprt &access_size)
168 exprt sum=object_offset;
188 const exprt &pointer,
190 const exprt &access_size)
201 exprt sum=object_offset;
222 const exprt &pointer,
The type of an expression, extends irept.
exprt size_of_expr(const typet &type, const namespacet &ns)
Semantic type conversion.
A base class for relations, i.e., binary predicates.
pointer_typet pointer_type(const typet &subtype)
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
The null pointer constant.
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
#define CHECK_RETURN(CONDITION)
exprt deallocated(const exprt &pointer, const namespacet &ns)
signedbv_typet signed_size_type()
exprt null_object(const exprt &pointer)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
exprt good_pointer(const exprt &pointer)
exprt object_size(const exprt &pointer)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
exprt pointer_object(const exprt &p)
API to expression classes.
exprt integer_address(const exprt &pointer)
Generic base class for unary expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
exprt object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Various predicates over pointers in programs.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
exprt malloc_object(const exprt &pointer, const namespacet &ns)
exprt dynamic_size(const namespacet &ns)
exprt invalid_pointer(const exprt &pointer)
Base class for all expressions.
exprt pointer_offset(const exprt &pointer)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
const typet & subtype() const
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().