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 
23 class dirtyt
24 {
25 private:
26  void die_if_uninitialized() const
27  {
28  INVARIANT(
30  "Uninitialized dirtyt. This dirtyt was constructed using the default "
31  "constructor and not subsequently initialized using "
32  "dirtyt::build().");
33  }
34 
35 public:
38 
43  dirtyt() : initialized(false)
44  {
45  }
46 
47  explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
48  {
49  build(goto_function);
50  initialized = true;
51  }
52 
53  explicit dirtyt(const goto_functionst &goto_functions) : initialized(false)
54  {
55  build(goto_functions);
56  // build(g_funs) responsible for setting initialized to true, since
57  // it is public and can be called independently
58  }
59 
60  void output(std::ostream &out) const;
61 
62  bool operator()(const irep_idt &id) const
63  {
65  return dirty.find(id)!=dirty.end();
66  }
67 
68  bool operator()(const symbol_exprt &expr) const
69  {
71  return operator()(expr.get_identifier());
72  }
73 
74  const std::unordered_set<irep_idt> &get_dirty_ids() const
75  {
77  return dirty;
78  }
79 
80  void add_function(const goto_functiont &goto_function)
81  {
82  build(goto_function);
83  initialized = true;
84  }
85 
86  void build(const goto_functionst &goto_functions)
87  {
88  // dirtyts should not be initialized twice
90  forall_goto_functions(it, goto_functions)
91  build(it->second);
92  initialized = true;
93  }
94 
95 protected:
96  void build(const goto_functiont &goto_function);
97 
98  // variables whose address is taken
99  std::unordered_set<irep_idt> dirty;
100 
101  void find_dirty(const exprt &expr);
102  void find_dirty_address_of(const exprt &expr);
103 };
104 
105 inline std::ostream &operator<<(
106  std::ostream &out,
107  const dirtyt &dirty)
108 {
109  dirty.output(out);
110  return out;
111 }
112 
116 {
117 public:
119  const irep_idt &id, const goto_functionst::goto_functiont &function);
120 
121  bool operator()(const irep_idt &id) const
122  {
123  return dirty(id);
124  }
125 
126  bool operator()(const symbol_exprt &expr) const
127  {
128  return dirty(expr);
129  }
130 
131 private:
133  std::unordered_set<irep_idt> dirty_processed_functions;
134 };
135 
136 #endif // CPROVER_ANALYSES_DIRTY_H
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:80
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:105
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:40
bool operator()(const irep_idt &id) const
Definition: dirty.h:121
void die_if_uninitialized() const
Definition: dirty.h:26
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Goto Programs with Functions.
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:37
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:115
void build(const goto_functionst &goto_functions)
Definition: dirty.h:86
API to expression classes.
bool initialized
Definition: dirty.h:36
::goto_functiont goto_functiont
bool operator()(const irep_idt &id) const
Definition: dirty.h:62
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:126
dirtyt(const goto_functionst &goto_functions)
Definition: dirty.h:53
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn&#39;t been seen before.
Definition: dirty.cpp:80
void find_dirty(const exprt &expr)
Definition: dirty.cpp:27
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const std::unordered_set< irep_idt > & get_dirty_ids() const
Definition: dirty.h:74
Base class for all expressions.
Definition: expr.h:42
dirtyt dirty
Definition: dirty.h:132
Definition: dirty.h:23
std::unordered_set< irep_idt > dirty
Definition: dirty.h:99
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:133
dirtyt()
Definition: dirty.h:43
Expression to hold a symbol (variable)
Definition: std_expr.h:90
#define forall_goto_functions(it, functions)
void output(std::ostream &out) const
Definition: dirty.cpp:70
dirtyt(const goto_functiont &goto_function)
Definition: dirty.h:47
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:68