cprover
dirty.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Variables whose address is taken
4 
5 Author: Daniel Kroening
6 
7 Date: 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 
26 class dirtyt
27 {
28 private:
29  void die_if_uninitialized() const
30  {
31  INVARIANT(
33  "Uninitialized dirtyt. This dirtyt was constructed using the default "
34  "constructor and not subsequently initialized using "
35  "dirtyt::build().");
36  }
37 
38 public:
41 
46  dirtyt() : initialized(false)
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 
98 protected:
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 
108 inline std::ostream &operator<<(
109  std::ostream &out,
110  const dirtyt &dirty)
111 {
112  dirty.output(out);
113  return out;
114 }
115 
119 {
120 public:
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 
134 private:
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:27
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:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:108
Goto Programs with Functions.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.