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 
23 {
24 public:
25  // Note: this currently doesn't specify a source language
26  // for the final argument to value_set_dereferencet.
27  // This means that language-inappropriate values such as
28  // (struct A*)some_integer_value in Java, may be returned.
30  const namespacet &_ns,
31  symbol_tablet &_new_symbol_table,
32  const optionst &_options,
33  value_setst &_value_sets):
34  options(_options),
35  ns(_ns),
36  value_sets(_value_sets),
37  dereference(_ns, _new_symbol_table, _options, *this, ID_nil, false)
38  {
39  }
40 
43  bool checks_only=false);
44 
46  goto_functionst &goto_functions,
47  bool checks_only=false);
48 
50  void pointer_checks(goto_functionst &goto_functions);
51 
54  exprt &expr);
55 
57  {
58  }
59 
60 protected:
61  const optionst &options;
62  const namespacet &ns;
65 
66  virtual bool is_valid_object(const irep_idt &identifier);
67 
68  virtual bool has_failed_symbol(
69  const exprt &expr,
70  const symbolt *&symbol);
71 
72  virtual void dereference_failure(
73  const std::string &property,
74  const std::string &msg,
75  const guardt &guard);
76 
77  virtual void get_value_set(const exprt &expr, value_setst::valuest &dest);
78 
81  bool checks_only=false);
82 
83 protected:
84  void dereference_rec(
85  exprt &expr, guardt &guard, const value_set_dereferencet::modet mode);
86  void dereference_expr(
87  exprt &expr,
88  const bool checks_only,
90 
91 #if 0
92  const std::set<irep_idt> *valid_local_variables;
93 #endif
96 
97  std::set<exprt> assertions;
99 };
100 
101 void dereference(
103  exprt &expr,
104  const namespacet &,
105  value_setst &);
106 
107 void remove_pointers(
108  goto_modelt &,
109  value_setst &);
110 
111 void remove_pointers(
112  goto_functionst &,
113  symbol_tablet &,
114  value_setst &);
115 
116 void pointer_checks(
117  goto_programt &,
118  symbol_tablet &,
119  const optionst &,
120  value_setst &);
121 
122 void pointer_checks(
123  goto_functionst &,
124  symbol_tablet &,
125  const optionst &,
126  value_setst &);
127 
128 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
virtual bool is_valid_object(const irep_idt &identifier)
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
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void dereference_rec(exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
Pointer Dereferencing.
void remove_pointers(goto_modelt &, value_setst &)
virtual void get_value_set(const exprt &expr, value_setst::valuest &dest)
void pointer_checks(goto_programt &goto_program)
Symbol Table + CFG.
Value Set Propagation.
instructionst::iterator targett
Definition: goto_program.h:397
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
void dereference_expression(goto_programt::const_targett target, exprt &expr)
value_set_dereferencet dereference
void dereference_program(goto_programt &goto_program, bool checks_only=false)
Base class for all expressions.
Definition: expr.h:42
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
goto_programt & goto_program
Definition: cover.cpp:63
std::list< exprt > valuest
Definition: value_sets.h:28
void pointer_checks(goto_programt &, symbol_tablet &, const optionst &, value_setst &)
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &)