Go to the documentation of this file.
12 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
13 #define CPROVER_UTIL_POINTER_PREDICATES_H
18 #define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
45 const
exprt &access_size);
51 const
exprt &access_size);
65 return base.
id() == ID_is_invalid_pointer;
73 #endif // CPROVER_UTIL_POINTER_PREDICATES_H
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &, const exprt &access_size)
Evaluates to true if the operand is a pointer to a dynamic object.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Base class for all expressions.
bool can_cast_expr< is_invalid_pointer_exprt >(const exprt &base)
exprt dynamic_object(const exprt &pointer)
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
exprt dead_object(const exprt &pointer, const namespacet &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt malloc_object(const exprt &pointer, const namespacet &)
exprt good_pointer_def(const exprt &pointer, const namespacet &)
exprt deallocated(const exprt &pointer, const namespacet &)
const irep_idt & id() const
void remove(const irep_namet &name)
#define SINCE(year, month, day, msg)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt integer_address(const exprt &pointer)
exprt null_object(const exprt &pointer)
exprt pointer_object(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt object_size(const exprt &pointer)
is_invalid_pointer_exprt(exprt pointer)
exprt dynamic_size(const namespacet &)
void validate_expr(const is_invalid_pointer_exprt &value)
API to expression classes.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
exprt good_pointer(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
exprt pointer_offset(const exprt &pointer)