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.
exprt size_of_expr(const typet &type, const namespacet &ns)
A generic 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)
The null pointer constant.
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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
exprt pointer_object(const exprt &p)
API to expression classes.
exprt integer_address(const exprt &pointer)
Generic base class for unary expressions.
exprt object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
const typet & follow(const typet &) const
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 generic 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)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().