cprover
value_set_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_VALUE_SET_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
14 
15 #include <unordered_set>
16 
17 #include <util/std_expr.h>
18 
19 #include "dereference_callback.h"
20 
21 class symbol_tablet;
22 class guardt;
23 class optionst;
24 class modet;
25 class symbolt;
26 
30 {
31 public:
40  const namespacet &_ns,
41  symbol_tablet &_new_symbol_table,
42  const optionst &_options,
43  dereference_callbackt &_dereference_callback,
44  const irep_idt _language_mode):
45  ns(_ns),
46  new_symbol_table(_new_symbol_table),
47  options(_options),
48  dereference_callback(_dereference_callback),
49  language_mode(_language_mode)
50  { }
51 
53 
54  enum class modet { READ, WRITE };
55 
70  virtual exprt dereference(
71  const exprt &pointer,
72  const guardt &guard,
73  const modet mode);
74 
77  static bool has_dereference(const exprt &expr);
78 
79  typedef std::unordered_set<exprt, irep_hash> expr_sett;
80 
81 private:
82  const namespacet &ns;
84  const optionst &options;
89  static unsigned invalid_counter;
90 
92  const typet &object_type,
93  const typet &dereference_type) const;
94 
95  void offset_sum(
96  exprt &dest,
97  const exprt &offset) const;
98 
99  class valuet
100  {
101  public:
104 
106  {
107  }
108  };
109 
110  valuet build_reference_to(
111  const exprt &what,
112  const modet mode,
113  const exprt &pointer,
114  const guardt &guard);
115 
116  bool get_value_guard(
117  const exprt &symbol,
118  const exprt &premise,
119  exprt &value);
120 
121  static const exprt &get_symbol(const exprt &object);
122 
123  void bounds_check(const index_exprt &expr, const guardt &guard);
124  void valid_check(const exprt &expr, const guardt &guard, const modet mode);
125 
126  void invalid_pointer(const exprt &expr, const guardt &guard);
127 
128  bool memory_model(
129  exprt &value,
130  const typet &type,
131  const guardt &guard,
132  const exprt &offset);
133 
135  exprt &value,
136  const typet &type,
137  const guardt &guard,
138  const exprt &offset);
139 
140  bool memory_model_bytes(
141  exprt &value,
142  const typet &type,
143  const guardt &guard,
144  const exprt &offset);
145 };
146 
147 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
The type of an expression.
Definition: type.h:20
Pointer Dereferencing.
static const exprt & get_symbol(const exprt &object)
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
dereference_callbackt & dereference_callback
void invalid_pointer(const exprt &expr, const guardt &guard)
Definition: guard.h:19
bool memory_model(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void valid_check(const exprt &expr, const guardt &guard, const modet mode)
void bounds_check(const index_exprt &expr, const guardt &guard)
bool memory_model_bytes(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
The NIL expression.
Definition: std_expr.h:3764
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
The boolean constant false.
Definition: std_expr.h:3753
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode)
Constructor.
Base class for all expressions.
Definition: expr.h:46
static bool has_dereference(const exprt &expr)
Returns &#39;true&#39; iff the given expression contains unary &#39;*&#39;.
symbol_tablet & new_symbol_table
void offset_sum(exprt &dest, const exprt &offset) const
bool get_value_guard(const exprt &symbol, const exprt &premise, exprt &value)
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
bool memory_model_conversion(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::unordered_set< exprt, irep_hash > expr_sett
array index operator
Definition: std_expr.h:1170