CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
pointer_predicates.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Various predicates over pointers in programs
4
5Author: 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
19exprt same_object(const exprt &p1, const exprt &p2);
20exprt deallocated(const exprt &pointer, const namespacet &);
21exprt dead_object(const exprt &pointer, const namespacet &);
22exprt pointer_offset(const exprt &pointer);
23exprt pointer_object(const exprt &pointer);
24exprt object_size(const exprt &pointer);
25exprt null_object(const exprt &pointer);
26
27exprt integer_address(const exprt &pointer);
29 const exprt &pointer,
30 const exprt &offset);
32 const exprt &pointer,
33 const exprt &access_size);
34
36{
37public:
40 {
41 }
42};
43
44template <>
46{
47 return base.id() == ID_is_invalid_pointer;
48}
49
50inline 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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:91
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
STL namespace.
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.