cprover
Loading...
Searching...
No Matches
goto_program_dereference.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set
4
5Author: 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/message.h>
16
19
20class exprt;
21class goto_functionst;
22class goto_modelt;
23class namespacet;
24class optionst;
26class symbolt;
27class value_setst;
28
32{
33public:
34 // Note: this currently doesn't specify a source language
35 // for the final argument to value_set_dereferencet.
36 // This means that language-inappropriate values such as
37 // (struct A*)some_integer_value in Java, may be returned.
38 // Note: value_set_dereferencet requires a messaget instance
39 // as on of its arguments to display the points-to set
40 // during symex. Display is not done during goto-program
41 // conversion. To ensure this the display_points_to_sets
42 // parameter in value_set_dereferencet::dereference()
43 // is set to false by default and is not changed by the
44 // goto program conversion modules. Similarly, here we set
45 // _log to be a default messaget instance.
58
60 goto_programt &goto_program,
61 bool checks_only=false);
62
64 goto_functionst &goto_functions,
65 bool checks_only=false);
66
68 const irep_idt &function_id,
70 exprt &expr);
71
73 {
74 }
75
76protected:
78 const namespacet &ns;
81
82 const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
83
84 std::vector<exprt> get_value_set(const exprt &expr) const override;
85
88 bool checks_only=false);
89
90protected:
91 void dereference_rec(exprt &expr);
92 void dereference_expr(exprt &expr, const bool checks_only);
93
97};
98
99void dereference(
100 const irep_idt &function_id,
102 exprt &expr,
103 const namespacet &,
104 value_setst &);
105
106void remove_pointers(
107 goto_modelt &,
108 value_setst &);
109
110#define OPT_REMOVE_POINTERS "(remove-pointers)"
111
112#define HELP_REMOVE_POINTERS \
113 " {y--remove-pointers} \t " \
114 "converts pointer arithmetic to base+offset expressions\n"
115
116#endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
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.
goto_program_dereferencet(const namespacet &_ns, symbol_table_baset &_new_symbol_table, const optionst &_options, value_setst &_value_sets, const messaget &_log=messaget())
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
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.
instructionst::iterator targett
instructionst::const_iterator const_targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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 remove_pointers(goto_modelt &, value_setst &)
Remove dereferences in all expressions contained in the program goto_model.
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...
Pointer Dereferencing.