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 
75  typedef std::unordered_set<exprt, irep_hash> expr_sett;
76 
77 private:
78  const namespacet &ns;
80  const optionst &options;
85  static unsigned invalid_counter;
86 
88  const typet &object_type,
89  const typet &dereference_type) const;
90 
91  void offset_sum(
92  exprt &dest,
93  const exprt &offset) const;
94 
95  class valuet
96  {
97  public:
100 
102  {
103  }
104  };
105 
106  valuet build_reference_to(
107  const exprt &what,
108  const modet mode,
109  const exprt &pointer,
110  const guardt &guard);
111 
112  bool get_value_guard(
113  const exprt &symbol,
114  const exprt &premise,
115  exprt &value);
116 
117  static const exprt &get_symbol(const exprt &object);
118 
119  void bounds_check(const index_exprt &expr, const guardt &guard);
120  void valid_check(const exprt &expr, const guardt &guard, const modet mode);
121 
122  void invalid_pointer(const exprt &expr, const guardt &guard);
123 
124  bool memory_model(
125  exprt &value,
126  const typet &type,
127  const guardt &guard,
128  const exprt &offset);
129 
131  exprt &value,
132  const typet &type,
133  const guardt &guard,
134  const exprt &offset);
135 
136  bool memory_model_bytes(
137  exprt &value,
138  const typet &type,
139  const guardt &guard,
140  const exprt &offset);
141 };
142 
143 #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)
The NIL expression.
Definition: std_expr.h:4510
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
The boolean constant false.
Definition: std_expr.h:4499
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: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)
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:1462