cprover
dereference.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Dereferencing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
14 
15 #include <util/namespace.h>
16 #include <util/expr.h>
17 
18 class if_exprt;
19 class typecast_exprt;
20 
23 {
24 public:
25  explicit dereferencet(
26  const namespacet &_ns):
27  ns(_ns)
28  {
29  }
30 
32 
36  exprt operator()(const exprt &pointer);
37 
38 private:
39  const namespacet &ns;
40 
42  const exprt &address,
43  const exprt &offset,
44  const typet &type);
45 
47  const if_exprt &expr,
48  const exprt &offset,
49  const typet &type);
50 
52  const exprt &expr,
53  const exprt &offset,
54  const typet &type);
55 
57  const typecast_exprt &expr,
58  const exprt &offset,
59  const typet &type);
60 
61  bool type_compatible(
62  const typet &object_type,
63  const typet &dereference_type) const;
64 
66  const exprt &object,
67  const exprt &offset,
68  const typet &type);
69 };
70 
75 inline exprt dereference(const exprt &pointer, const namespacet &ns)
76 {
77  dereferencet dereference_object(ns);
78  return dereference_object(pointer);
79 }
80 
81 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
dereferencet::dereference_typecast
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Definition: dereference.cpp:276
typet
The type of an expression, extends irept.
Definition: type.h:27
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
dereferencet::read_object
exprt read_object(const exprt &object, const exprt &offset, const typet &type)
Definition: dereference.cpp:50
exprt
Base class for all expressions.
Definition: expr.h:54
namespace.h
dereferencet::dereferencet
dereferencet(const namespacet &_ns)
Definition: dereference.h:25
dereferencet::operator()
exprt operator()(const exprt &pointer)
Dereference the given pointer-expression.
Definition: dereference.cpp:28
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
dereferencet::dereference_plus
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Definition: dereference.cpp:233
dereferencet::ns
const namespacet & ns
Definition: dereference.h:39
dereferencet
Wrapper for a function which dereference a pointer-expression.
Definition: dereference.h:22
dereferencet::dereference_rec
exprt dereference_rec(const exprt &address, const exprt &offset, const typet &type)
Attempt to dereference the object at address address + offset and of type type.
Definition: dereference.cpp:157
dereference
exprt dereference(const exprt &pointer, const namespacet &ns)
Dereference the given pointer-expression.
Definition: dereference.h:75
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
dereferencet::~dereferencet
~dereferencet()
Definition: dereference.h:31
dereferencet::type_compatible
bool type_compatible(const typet &object_type, const typet &dereference_type) const
Check that it is ok to cast an object of type object_type to deference_type.
Definition: dereference.cpp:307
dereferencet::dereference_if
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Definition: dereference.cpp:218