CBMC
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 "dereference_callback.h"
16 #include "value_set_dereference.h"
17 
18 class exprt;
19 class goto_functionst;
20 class goto_modelt;
21 class namespacet;
22 class optionst;
23 class symbol_table_baset;
24 class symbolt;
25 class value_setst;
26 
30 {
31 public:
32  // Note: this currently doesn't specify a source language
33  // for the final argument to value_set_dereferencet.
34  // This means that language-inappropriate values such as
35  // (struct A*)some_integer_value in Java, may be returned.
36  // Note: value_set_dereferencet requires a message_handlert instance
37  // as one of its arguments to display the points-to set
38  // during symex. Display is not done during goto-program
39  // conversion. To ensure this the display_points_to_sets
40  // parameter in value_set_dereferencet::dereference()
41  // is set to false by default and is not changed by the
42  // goto program conversion modules.
44  const namespacet &_ns,
45  symbol_table_baset &_new_symbol_table,
46  const optionst &_options,
47  value_setst &_value_sets,
48  message_handlert &message_handler)
49  : options(_options),
50  ns(_ns),
51  value_sets(_value_sets),
52  dereference(_ns, _new_symbol_table, *this, ID_nil, false, message_handler)
53  {
54  }
55 
57  goto_programt &goto_program,
58  bool checks_only=false);
59 
61  goto_functionst &goto_functions,
62  bool checks_only=false);
63 
65  const irep_idt &function_id,
67  exprt &expr);
68 
70  {
71  }
72 
73 protected:
74  const optionst &options;
75  const namespacet &ns;
78 
79  const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
80 
81  std::vector<exprt> get_value_set(const exprt &expr) const override;
82 
85  bool checks_only=false);
86 
87 protected:
88  void dereference_rec(exprt &expr);
89  void dereference_expr(exprt &expr, const bool checks_only);
90 
94 };
95 
96 void dereference(
97  const irep_idt &function_id,
99  exprt &expr,
100  const namespacet &,
101  value_setst &,
102  message_handlert &);
103 
105 
106 #define OPT_REMOVE_POINTERS "(remove-pointers)"
107 
108 #define HELP_REMOVE_POINTERS \
109  " {y--remove-pointers} \t " \
110  "converts pointer arithmetic to base+offset expressions\n"
111 
112 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
Base class for pointer value set analysis.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
A collection of goto functions.
Wrapper for functions removing dereferences in expressions contained in a goto program.
void dereference_program(goto_programt &goto_program, bool checks_only=false)
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
void dereference_expr(exprt &expr, const bool checks_only)
Remove dereference expressions contained in expr.
value_set_dereferencet dereference
std::vector< exprt > get_value_set(const exprt &expr) const override
Gets the value set corresponding to the current target and expression expr.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
void dereference_rec(exprt &expr)
Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *...
goto_programt::const_targett current_target
goto_program_dereferencet(const namespacet &_ns, symbol_table_baset &_new_symbol_table, const optionst &_options, value_setst &_value_sets, message_handlert &message_handler)
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.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
Wrapper for a function dereferencing pointer expressions using a value set.
Pointer Dereferencing.
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &, message_handlert &)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
void remove_pointers(goto_modelt &, value_setst &, message_handlert &)
Remove dereferences in all expressions contained in the program goto_model.
Pointer Dereferencing.