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.
31  // Note: value_set_dereferencet requires a messaget instance
32  // as on of its arguments to display the points-to set
33  // during symex. Display is not done during goto-program
34  // conversion. To ensure this the display_points_to_sets
35  // parameter in value_set_dereferencet::dereference()
36  // is set to false by default and is not changed by the
37  // goto program conversion modules. Similarly, here we set
38  // _log to be a default messaget instance.
40  const namespacet &_ns,
41  symbol_tablet &_new_symbol_table,
42  const optionst &_options,
43  value_setst &_value_sets,
44  const messaget &_log = messaget())
45  : options(_options),
46  ns(_ns),
47  value_sets(_value_sets),
48  dereference(_ns, _new_symbol_table, *this, ID_nil, false, _log)
49  {
50  }
51 
53  goto_programt &goto_program,
54  bool checks_only=false);
55 
57  goto_functionst &goto_functions,
58  bool checks_only=false);
59 
61  const irep_idt &function_id,
63  exprt &expr);
64 
66  {
67  }
68 
69 protected:
70  const optionst &options;
71  const namespacet &ns;
74 
75  const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
76 
77  std::vector<exprt> get_value_set(const exprt &expr) const override;
78 
81  bool checks_only=false);
82 
83 protected:
84  void dereference_rec(exprt &expr);
85  void dereference_expr(exprt &expr, const bool checks_only);
86 
90 };
91 
92 void dereference(
93  const irep_idt &function_id,
95  exprt &expr,
96  const namespacet &,
97  value_setst &);
98 
99 void remove_pointers(
100  goto_modelt &,
101  value_setst &);
102 
103 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_program_dereferencet::goto_program_dereferencet
goto_program_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, value_setst &_value_sets, const messaget &_log=messaget())
Definition: goto_program_dereference.h:39
goto_program_dereferencet::dereference_expression
void dereference_expression(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
Definition: goto_program_dereference.cpp:256
remove_pointers
void remove_pointers(goto_modelt &, value_setst &)
Remove dereferences in all expressions contained in the program goto_model.
Definition: goto_program_dereference.cpp:269
optionst
Definition: options.h:23
value_set_dereference.h
Pointer Dereferencing.
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:28
dereference
void dereference(const irep_idt &function_id, 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...
Definition: goto_program_dereference.cpp:287
goto_program_dereferencet::options
const optionst & options
Definition: goto_program_dereference.h:70
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
goto_program_dereferencet::value_sets
value_setst & value_sets
Definition: goto_program_dereference.h:72
namespace.h
goto_program_dereferencet::dereference_expr
void dereference_expr(exprt &expr, const bool checks_only)
Remove dereference expressions contained in expr.
Definition: goto_program_dereference.cpp:144
goto_program_dereferencet::dereference
value_set_dereferencet dereference
Definition: goto_program_dereference.h:73
value_sets.h
Value Set Propagation.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_program_dereferencet::get_value_set
std::vector< exprt > get_value_set(const exprt &expr) const override
Gets the value set corresponding to the current target and expression expr.
Definition: goto_program_dereference.cpp:134
goto_program_dereferencet
Wrapper for functions removing dereferences in expressions contained in a goto program.
Definition: goto_program_dereference.h:25
value_set_dereferencet
Wrapper for a function dereferencing pointer expressions using a value set.
Definition: value_set_dereference.h:28
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
value_setst
Definition: value_sets.h:22
goto_program_dereferencet::dereference_instruction
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
Definition: goto_program_dereference.cpp:194
goto_program_dereferencet::get_or_create_failed_symbol
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Definition: goto_program_dereference.cpp:24
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_program_dereferencet::dereference_program
void dereference_program(goto_programt &goto_program, bool checks_only=false)
Definition: goto_program_dereference.cpp:157
goto_program_dereferencet::new_code
goto_programt new_code
Definition: goto_program_dereference.h:89
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
goto_program_dereferencet::current_target
goto_programt::const_targett current_target
Definition: goto_program_dereference.h:88
goto_program_dereferencet::current_function
irep_idt current_function
Definition: goto_program_dereference.h:87
goto_program_dereferencet::dereference_rec
void dereference_rec(exprt &expr)
Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *...
Definition: goto_program_dereference.cpp:49
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550
goto_program_dereferencet::ns
const namespacet & ns
Definition: goto_program_dereference.h:71
goto_program_dereferencet::~goto_program_dereferencet
virtual ~goto_program_dereferencet()
Definition: goto_program_dereference.h:65