cprover
goto_program_dereference.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
14 
15 #include <util/namespace.h>
16 
18 
19 #include "value_sets.h"
20 #include "value_set_dereference.h"
21 
25 {
26 public:
27  // Note: this currently doesn't specify a source language
28  // for the final argument to value_set_dereferencet.
29  // This means that language-inappropriate values such as
30  // (struct A*)some_integer_value in Java, may be returned.
32  const namespacet &_ns,
33  symbol_tablet &_new_symbol_table,
34  const optionst &_options,
35  value_setst &_value_sets)
36  : options(_options),
37  ns(_ns),
38  value_sets(_value_sets),
39  dereference(_ns, _new_symbol_table, *this, ID_nil, false)
40  {
41  }
42 
44  goto_programt &goto_program,
45  bool checks_only=false);
46 
48  goto_functionst &goto_functions,
49  bool checks_only=false);
50 
51  void pointer_checks(goto_programt &goto_program);
52  void pointer_checks(goto_functionst &goto_functions);
53 
56  exprt &expr);
57 
59  {
60  }
61 
62 protected:
63  const optionst &options;
64  const namespacet &ns;
67 
68  DEPRECATED("Unused")
69  virtual bool is_valid_object(const irep_idt &identifier);
70 
71  bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override;
72 
73  DEPRECATED("Unused")
74  virtual void dereference_failure(
75  const std::string &property,
76  const std::string &msg,
77  const guardt &guard);
78 
79  void get_value_set(const exprt &expr, value_setst::valuest &dest) override;
80 
82  goto_programt::targett target,
83  bool checks_only=false);
84 
85 protected:
86  void dereference_rec(
87  exprt &expr, guardt &guard, const value_set_dereferencet::modet mode);
88  void dereference_expr(
89  exprt &expr,
90  const bool checks_only,
91  const value_set_dereferencet::modet mode);
92 
93 #if 0
94  const std::set<irep_idt> *valid_local_variables;
95 #endif
97 
100 
102  std::set<exprt> assertions;
103 
106 };
107 
108 void dereference(
110  exprt &expr,
111  const namespacet &,
112  value_setst &);
113 
114 void remove_pointers(
115  goto_modelt &,
116  value_setst &);
117 
118 DEPRECATED("Unused")
119 void remove_pointers(
120  goto_functionst &,
121  symbol_tablet &,
122  value_setst &);
123 
124 DEPRECATED("Unused")
125 void pointer_checks(
126  goto_programt &,
127  symbol_tablet &,
128  const optionst &,
129  value_setst &);
130 
131 DEPRECATED("Unused")
132 void pointer_checks(
133  goto_functionst &,
134  symbol_tablet &,
135  const optionst &,
136  value_setst &);
137 
138 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
std::set< exprt > assertions
Unused.
Base class for pointer value set analysis.
virtual bool is_valid_object(const irep_idt &identifier)
void get_value_set(const exprt &expr, value_setst::valuest &dest) override
Gets the value set corresponding to the current target and expression expr.
source_locationt dereference_location
Unused.
goto_programt::const_targett current_target
goto_program_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, value_setst &_value_sets)
Definition: guard.h:19
STL namespace.
Symbol table entry.
Definition: symbol.h:27
void dereference_rec(exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
Turn subexpression of expr of the form &*p or reference_to(*p) to p and use dereference on subexpress...
Pointer Dereferencing.
void remove_pointers(goto_modelt &, value_setst &)
Remove dereferences in all expressions contained in the program goto_model.
void pointer_checks(goto_programt &goto_program)
Throw an exception in case removing dereferences from the program would throw an exception.
Symbol Table + CFG.
Value Set Propagation.
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
A collection of goto functions.
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Wrapper for functions removing dereferences in expressions contained in a goto program.
#define DEPRECATED(msg)
Definition: deprecate.h:23
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
Remove dereference expressions contained in expr.
void dereference_expression(goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
value_set_dereferencet dereference
void dereference_program(goto_programt &goto_program, bool checks_only=false)
Base class for all expressions.
Definition: expr.h:54
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
void pointer_checks(goto_programt &, symbol_tablet &, const optionst &, value_setst &)
Wrapper for a function dereferencing pointer expressions using a value set.
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...