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 "std_expr.h"
16 
17 #define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
18 
19 exprt same_object(const exprt &p1, const exprt &p2);
20 exprt deallocated(const exprt &pointer, const namespacet &);
21 exprt dead_object(const exprt &pointer, const namespacet &);
23 exprt pointer_offset(const exprt &pointer);
24 exprt pointer_object(const exprt &pointer);
25 exprt malloc_object(const exprt &pointer, const namespacet &);
26 exprt object_size(const exprt &pointer);
27 exprt dynamic_object(const exprt &pointer);
28 exprt good_pointer(const exprt &pointer);
29 exprt good_pointer_def(const exprt &pointer, const namespacet &);
30 exprt null_object(const exprt &pointer);
31 exprt null_pointer(const exprt &pointer);
32 exprt integer_address(const exprt &pointer);
34  const exprt &pointer,
35  const exprt &offset);
37  const exprt &pointer,
38  const namespacet &,
39  const exprt &access_size);
41  const exprt &pointer,
42  const exprt &offset);
44  const exprt &pointer,
45  const exprt &access_size);
46 
48 {
49 public:
50  explicit is_invalid_pointer_exprt(exprt pointer)
51  : unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)}
52  {
53  }
54 };
55 
56 #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:149
exprt
Base class for all expressions.
Definition: expr.h:53
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
dynamic_object_lower_bound
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:142
dead_object
exprt dead_object(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:58
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:42
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:83
deallocated
exprt deallocated(const exprt &pointer, const namespacet &)
Definition: pointer_predicates.cpp:50
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:208
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:178
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:129
null_object
exprt null_object(const exprt &pointer)
Definition: pointer_predicates.cpp:123
pointer_object
exprt pointer_object(const exprt &pointer)
Definition: pointer_predicates.cpp:22
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:27
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
is_invalid_pointer_exprt::is_invalid_pointer_exprt
is_invalid_pointer_exprt(exprt pointer)
Definition: pointer_predicates.h:50
dynamic_size
exprt dynamic_size(const namespacet &)
Definition: pointer_predicates.cpp:66
is_invalid_pointer_exprt
Definition: pointer_predicates.h:48
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:546
good_pointer
exprt good_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:78
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:136
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37