CBMC
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 &);
22 exprt pointer_offset(const exprt &pointer);
23 exprt pointer_object(const exprt &pointer);
24 exprt object_size(const exprt &pointer);
25 exprt null_object(const exprt &pointer);
26 
27 exprt integer_address(const exprt &pointer);
29  const exprt &pointer,
30  const exprt &offset);
32  const exprt &pointer,
33  const exprt &access_size);
34 
36 {
37 public:
38  explicit is_invalid_pointer_exprt(exprt pointer)
39  : unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)}
40  {
41  }
42 };
43 
44 template <>
46 {
47  return base.id() == ID_is_invalid_pointer;
48 }
49 
50 inline void validate_expr(const is_invalid_pointer_exprt &value)
51 {
52  validate_operands(value, 1, "is_invalid_pointer must have one operand");
53 }
54 
55 #endif // CPROVER_UTIL_POINTER_PREDICATES_H
Base class for all expressions.
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:388
is_invalid_pointer_exprt(exprt pointer)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt dead_object(const exprt &pointer, const namespacet &)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
void validate_expr(const is_invalid_pointer_exprt &value)
exprt deallocated(const exprt &pointer, const namespacet &)
exprt same_object(const exprt &p1, const exprt &p2)
bool can_cast_expr< is_invalid_pointer_exprt >(const exprt &base)
exprt pointer_object(const exprt &pointer)
exprt null_object(const exprt &pointer)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
API to expression classes.