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:
44  const namespacet &_ns,
45  symbol_tablet &_new_symbol_table,
46  const optionst &_options,
47  dereference_callbackt &_dereference_callback,
48  const irep_idt _language_mode,
49  bool _exclude_null_derefs):
50  ns(_ns),
51  new_symbol_table(_new_symbol_table),
52  options(_options),
53  dereference_callback(_dereference_callback),
54  language_mode(_language_mode),
55  exclude_null_derefs(_exclude_null_derefs)
56  { }
57 
59 
60  enum class modet { READ, WRITE };
61 
76  virtual exprt dereference(
77  const exprt &pointer,
78  const guardt &guard,
79  const modet mode);
80 
81  typedef std::unordered_set<exprt, irep_hash> expr_sett;
82 
83 private:
84  const namespacet &ns;
86  const optionst &options;
93  const bool exclude_null_derefs;
94  static unsigned invalid_counter;
95 
97  const typet &object_type,
98  const typet &dereference_type) const;
99 
100  void offset_sum(
101  exprt &dest,
102  const exprt &offset) const;
103 
105  class valuet
106  {
107  public:
110  bool ignore;
111 
113  {
114  }
115  };
116 
136  valuet build_reference_to(
137  const exprt &what,
138  const modet mode,
139  const exprt &pointer,
140  const guardt &guard);
141 
142  bool get_value_guard(
143  const exprt &symbol,
144  const exprt &premise,
145  exprt &value);
146 
147  static const exprt &get_symbol(const exprt &object);
148 
149  void bounds_check(const index_exprt &expr, const guardt &guard);
150  void valid_check(const exprt &expr, const guardt &guard, const modet mode);
151 
152  void invalid_pointer(const exprt &expr, const guardt &guard);
153 
154  bool memory_model(
155  exprt &value,
156  const typet &type,
157  const guardt &guard,
158  const exprt &offset);
159 
161  exprt &value,
162  const typet &type,
163  const guardt &guard,
164  const exprt &offset);
165 
166  bool memory_model_bytes(
167  exprt &value,
168  const typet &type,
169  const guardt &guard,
170  const exprt &offset);
171 };
172 
173 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
The type of an expression.
Definition: type.h:22
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:30
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)
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs)
Constructor.
The NIL expression.
Definition: std_expr.h:4508
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
Get a guard and expression to access what under guard.
The boolean constant false.
Definition: std_expr.h:4497
Base class for all expressions.
Definition: expr.h:42
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)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::unordered_set< exprt, irep_hash > expr_sett
Return value for build_reference_to; see that method for documentation.
array index operator
Definition: std_expr.h:1462