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 class exprt;
16 class namespacet;
17 class typet;
18 
19 exprt same_object(const exprt &p1, const exprt &p2);
20 exprt deallocated(const exprt &pointer, const namespacet &ns);
21 exprt dead_object(const exprt &pointer, const namespacet &ns);
22 exprt dynamic_size(const namespacet &ns);
23 exprt pointer_offset(const exprt &pointer);
24 exprt malloc_object(const exprt &pointer, const namespacet &ns);
25 exprt object_size(const exprt &pointer);
27  const exprt &pointer, const typet &type, const namespacet &ns);
28 exprt dynamic_object(const exprt &pointer);
29 exprt good_pointer(const exprt &pointer);
30 exprt good_pointer_def(const exprt &pointer, const namespacet &ns);
31 exprt null_object(const exprt &pointer);
32 exprt null_pointer(const exprt &pointer);
33 exprt integer_address(const exprt &pointer);
34 exprt invalid_pointer(const exprt &pointer);
36  const exprt &pointer,
37  const namespacet &ns,
38  const exprt &offset);
40  const exprt &pointer,
41  const typet &dereference_type,
42  const namespacet &ns,
43  const exprt &access_size);
45  const exprt &pointer,
46  const namespacet &ns,
47  const exprt &offset);
49  const exprt &pointer,
50  const typet &dereference_type,
51  const namespacet &ns,
52  const exprt &access_size);
53 
54 #endif // CPROVER_UTIL_POINTER_PREDICATES_H
exprt invalid_pointer(const exprt &pointer)
The type of an expression.
Definition: type.h:20
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)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
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.
Definition: expr.h:46
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)