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 symbolt;
25 
28 {
29 public:
39  const namespacet &_ns,
40  symbol_tablet &_new_symbol_table,
41  dereference_callbackt &_dereference_callback,
42  const irep_idt _language_mode,
43  bool _exclude_null_derefs):
44  ns(_ns),
45  new_symbol_table(_new_symbol_table),
46  dereference_callback(_dereference_callback),
47  language_mode(_language_mode),
48  exclude_null_derefs(_exclude_null_derefs)
49  { }
50 
52 
53  enum class modet { READ, WRITE };
54 
63  virtual exprt dereference(
64  const exprt &pointer,
65  const guardt &guard,
66  const modet mode);
67 
68 private:
69  const namespacet &ns;
77  const bool exclude_null_derefs;
78 
80  const typet &object_type,
81  const typet &dereference_type) const;
82 
84  class valuet
85  {
86  public:
89  bool ignore;
90 
92  {
93  }
94  };
95 
96  valuet build_reference_to(const exprt &what, const exprt &pointer);
97 
98  bool memory_model(exprt &value, const typet &type, const exprt &offset);
99 
100  bool memory_model_bytes(
101  exprt &value,
102  const typet &type,
103  const exprt &offset);
104 };
105 
106 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
value_set_dereferencet::valuet
Return value for build_reference_to; see that method for documentation.
Definition: value_set_dereference.h:84
value_set_dereferencet::valuet::pointer_guard
exprt pointer_guard
Definition: value_set_dereference.h:88
optionst
Definition: options.h:22
value_set_dereferencet::ns
const namespacet & ns
Definition: value_set_dereference.h:69
typet
The type of an expression, extends irept.
Definition: type.h:27
value_set_dereferencet::value_set_dereferencet
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs)
Definition: value_set_dereference.h:38
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:27
value_set_dereferencet::language_mode
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition: value_set_dereference.h:74
value_set_dereferencet::exclude_null_derefs
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
Definition: value_set_dereference.h:77
exprt
Base class for all expressions.
Definition: expr.h:54
value_set_dereferencet::dereference
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Dereference the given pointer-expression.
Definition: value_set_dereference.cpp:35
value_set_dereferencet::~value_set_dereferencet
virtual ~value_set_dereferencet()
Definition: value_set_dereference.h:51
value_set_dereferencet::modet::READ
@ READ
value_set_dereferencet::modet::WRITE
@ WRITE
value_set_dereferencet::new_symbol_table
symbol_tablet & new_symbol_table
Definition: value_set_dereference.h:70
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
guardt
Definition: guard.h:19
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
value_set_dereferencet::dereference_callback
dereference_callbackt & dereference_callback
Definition: value_set_dereference.h:71
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
value_set_dereferencet::memory_model_bytes
bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
Definition: value_set_dereference.cpp:567
value_set_dereferencet::valuet::valuet
valuet()
Definition: value_set_dereference.h:91
value_set_dereferencet
Wrapper for a function dereferencing pointer expressions using a value set.
Definition: value_set_dereference.h:27
value_set_dereferencet::dereference_type_compare
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
Definition: value_set_dereference.cpp:193
symbolt
Symbol table entry.
Definition: symbol.h:27
dereference_callback.h
value_set_dereferencet::modet
modet
Definition: value_set_dereference.h:53
value_set_dereferencet::valuet::ignore
bool ignore
Definition: value_set_dereference.h:89
value_set_dereferencet::memory_model
bool memory_model(exprt &value, const typet &type, const exprt &offset)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
Definition: value_set_dereference.cpp:521
std_expr.h
value_set_dereferencet::build_reference_to
valuet build_reference_to(const exprt &what, const exprt &pointer)
Definition: value_set_dereference.cpp:271
value_set_dereferencet::valuet::value
exprt value
Definition: value_set_dereference.h:87