cprover
Loading...
Searching...
No Matches
dirty.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Variables whose address is taken
4
5Author: Daniel Kroening
6
7Date: March 2013
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_ANALYSES_DIRTY_H
15#define CPROVER_ANALYSES_DIRTY_H
16
17#include <unordered_set>
18
19#include <util/std_expr.h>
20#include <util/invariant.h>
22
26class dirtyt
27{
28private:
30 {
33 "Uninitialized dirtyt. This dirtyt was constructed using the default "
34 "constructor and not subsequently initialized using "
35 "dirtyt::build().");
36 }
37
38public:
41
47 {
48 }
49
50 explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
51 {
52 build(goto_function);
53 initialized = true;
54 }
55
56 explicit dirtyt(const goto_functionst &goto_functions) : initialized(false)
57 {
58 build(goto_functions);
59 // build(g_funs) responsible for setting initialized to true, since
60 // it is public and can be called independently
61 }
62
63 void output(std::ostream &out) const;
64
65 bool operator()(const irep_idt &id) const
66 {
68 return dirty.find(id)!=dirty.end();
69 }
70
71 bool operator()(const symbol_exprt &expr) const
72 {
74 return operator()(expr.get_identifier());
75 }
76
77 const std::unordered_set<irep_idt> &get_dirty_ids() const
78 {
80 return dirty;
81 }
82
83 void add_function(const goto_functiont &goto_function)
84 {
85 build(goto_function);
86 initialized = true;
87 }
88
89 void build(const goto_functionst &goto_functions)
90 {
91 // dirtyts should not be initialized twice
93 for(const auto &gf_entry : goto_functions.function_map)
94 build(gf_entry.second);
95 initialized = true;
96 }
97
98protected:
99 void build(const goto_functiont &goto_function);
100
101 // variables whose address is taken
102 std::unordered_set<irep_idt> dirty;
103
104 void find_dirty(const exprt &expr);
105 void find_dirty_address_of(const exprt &expr);
106};
107
108inline std::ostream &operator<<(
109 std::ostream &out,
110 const dirtyt &dirty)
111{
112 dirty.output(out);
113 return out;
114}
115
119{
120public:
122 const irep_idt &id, const goto_functionst::goto_functiont &function);
123
124 bool operator()(const irep_idt &id) const
125 {
126 return dirty(id);
127 }
128
129 bool operator()(const symbol_exprt &expr) const
130 {
131 return dirty(expr);
132 }
133
134private:
136 std::unordered_set<irep_idt> dirty_processed_functions;
137};
138
139#endif // CPROVER_ANALYSES_DIRTY_H
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:71
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:83
void build(const goto_functionst &goto_functions)
Definition: dirty.h:89
void find_dirty(const exprt &expr)
Definition: dirty.cpp:25
bool operator()(const irep_idt &id) const
Definition: dirty.h:65
bool initialized
Definition: dirty.h:39
const std::unordered_set< irep_idt > & get_dirty_ids() const
Definition: dirty.h:77
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:38
void output(std::ostream &out) const
Definition: dirty.cpp:68
dirtyt(const goto_functionst &goto_functions)
Definition: dirty.h:56
std::unordered_set< irep_idt > dirty
Definition: dirty.h:102
dirtyt(const goto_functiont &goto_function)
Definition: dirty.h:50
dirtyt()
Definition: dirty.h:46
void die_if_uninitialized() const
Definition: dirty.h:29
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:40
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:119
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:129
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:136
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
Definition: dirty.cpp:78
bool operator()(const irep_idt &id) const
Definition: dirty.h:124
dirtyt dirty
Definition: dirty.h:135
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:108
Goto Programs with Functions.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.