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 
24 {
25 public:
33  explicit dereferencet(
34  const namespacet &_ns):
35  ns(_ns)
36  {
37  }
38 
40 
49  exprt operator()(const exprt &pointer);
50 
51 private:
52  const namespacet &ns;
53 
55  const exprt &address,
56  const exprt &offset,
57  const typet &type);
58 
60  const if_exprt &expr,
61  const exprt &offset,
62  const typet &type);
63 
65  const exprt &expr,
66  const exprt &offset,
67  const typet &type);
68 
70  const typecast_exprt &expr,
71  const exprt &offset,
72  const typet &type);
73 
74  bool type_compatible(
75  const typet &object_type,
76  const typet &dereference_type) const;
77 
78  void offset_sum(
79  exprt &dest,
80  const exprt &offset) const;
81 
83  const exprt &object,
84  const exprt &offset,
85  const typet &type);
86 };
87 
88 inline exprt dereference(const exprt &pointer, const namespacet &ns)
89 {
90  dereferencet dereference_object(ns);
91  return dereference_object(pointer);
92 }
93 
94 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
The type of an expression.
Definition: type.h:20
semantic type conversion
Definition: std_expr.h:1725
exprt dereference_rec(const exprt &address, const exprt &offset, const typet &type)
const namespacet & ns
Definition: dereference.h:52
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
bool type_compatible(const typet &object_type, const typet &dereference_type) const
exprt dereference(const exprt &pointer, const namespacet &ns)
Definition: dereference.h:88
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Base class for all expressions.
Definition: expr.h:46
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
TO_BE_DOCUMENTED.
Definition: dereference.h:23
dereferencet(const namespacet &_ns)
Constructor.
Definition: dereference.h:33
exprt operator()(const exprt &pointer)
Definition: dereference.cpp:30
void offset_sum(exprt &dest, const exprt &offset) const
exprt read_object(const exprt &object, const exprt &offset, const typet &type)
Definition: dereference.cpp:49