12 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H 13 #define CPROVER_UTIL_POINTER_PREDICATES_H 41 const typet &dereference_type,
43 const exprt &access_size);
50 const typet &dereference_type,
52 const exprt &access_size);
54 #endif // CPROVER_UTIL_POINTER_PREDICATES_H exprt invalid_pointer(const exprt &pointer)
The type of an expression.
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt null_pointer(const exprt &pointer)
exprt dynamic_object(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt pointer_object_has_type(const exprt &pointer, const typet &type, const namespacet &ns)
exprt object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
exprt malloc_object(const exprt &pointer, const namespacet &ns)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
exprt integer_address(const exprt &pointer)
Base class for all expressions.
exprt same_object(const exprt &p1, const exprt &p2)
exprt good_pointer(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt pointer_offset(const exprt &pointer)
exprt null_object(const exprt &pointer)
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
exprt dynamic_size(const namespacet &ns)