cprover
pointer_predicates.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Various predicates over pointers in programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
13 #define CPROVER_UTIL_POINTER_PREDICATES_H
14 
15 #include "deprecate.h"
16 #include "std_expr.h"
17 
18 #define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
19 
20 exprt same_object(const exprt &p1, const exprt &p2);
21 exprt deallocated(const exprt &pointer, const namespacet &);
22 exprt dead_object(const exprt &pointer, const namespacet &);
23 DEPRECATED(SINCE(2021, 5, 6, "Use object_size instead"))
25 exprt pointer_offset(const exprt &pointer);
26 exprt pointer_object(const exprt &pointer);
27 DEPRECATED(SINCE(2021, 5, 6, "Unnecessary, remove any use"))
28 exprt malloc_object(const exprt &pointer, const namespacet &);
29 exprt object_size(const exprt &pointer);
30 DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
31 exprt dynamic_object(const exprt &pointer);
32 exprt good_pointer(const exprt &pointer);
33 exprt good_pointer_def(const exprt &pointer, const namespacet &);
34 exprt null_object(const exprt &pointer);
35 exprt null_pointer(const exprt &pointer);
36 exprt integer_address(const exprt &pointer);
37 DEPRECATED(SINCE(2021, 5, 6, "Use object_lower_bound instead"))
39  const exprt &pointer,
40  const exprt &offset);
41 DEPRECATED(SINCE(2021, 5, 6, "Use object_upper_bound instead"))
43  const exprt &pointer,
44  const namespacet &,
45  const exprt &access_size);
47  const exprt &pointer,
48  const exprt &offset);
50  const exprt &pointer,
51  const exprt &access_size);
52 
54 {
55 public:
56  explicit is_invalid_pointer_exprt(exprt pointer)
57  : unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)}
58  {
59  }
60 };
61 
62 template <>
64 {
65  return base.id() == ID_is_invalid_pointer;
66 }
67 
68 inline void validate_expr(const is_invalid_pointer_exprt &value)
69 {
70  validate_operands(value, 1, "is_invalid_pointer must have one operand");
71 }
72 
73 #endif // CPROVER_UTIL_POINTER_PREDICATES_H
dynamic_object_upper_bound
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &, const exprt &access_size)
Definition: pointer_predicates.cpp:133
is_dynamic_object_exprt
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:301
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
exprt
Base class for all expressions.
Definition: expr.h:54
can_cast_expr< is_invalid_pointer_exprt >
bool can_cast_expr< is_invalid_pointer_exprt >(const exprt &base)
Definition: pointer_predicates.h:63
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:72
dynamic_object_lower_bound
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:126
dead_object
exprt dead_object(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:59
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:43
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:84
deprecate.h
deallocated
exprt deallocated(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:51
irept::id
const irep_idt & id() const
Definition: irep.h:407
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:96
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:192
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:162
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:113
null_object
exprt null_object(const exprt &pointer)
Definition: pointer_predicates.cpp:107
pointer_object
exprt pointer_object(const exprt &pointer)
Definition: pointer_predicates.cpp:23
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:28
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:33
is_invalid_pointer_exprt::is_invalid_pointer_exprt
is_invalid_pointer_exprt(exprt pointer)
Definition: pointer_predicates.h:56
dynamic_size
exprt dynamic_size(const namespacet &)
Definition: pointer_predicates.cpp:67
validate_expr
void validate_expr(const is_invalid_pointer_exprt &value)
Definition: pointer_predicates.h:68
is_invalid_pointer_exprt
Definition: pointer_predicates.h:54
std_expr.h
API to expression classes.
unary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:495
good_pointer
exprt good_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:79
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:120
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:38