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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
dirtyt::operator()
bool operator()(const irep_idt &id) const
Definition: dirty.h:62
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
incremental_dirtyt::dirty
dirtyt dirty
Definition: dirty.h:132
dirtyt
Definition: dirty.h:23
dirtyt::dirtyt
dirtyt(const goto_functiont &goto_function)
Definition: dirty.h:47
operator<<
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:105
dirtyt::add_function
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:80
exprt
Base class for all expressions.
Definition: expr.h:54
incremental_dirtyt::operator()
bool operator()(const irep_idt &id) const
Definition: dirty.h:121
dirtyt::get_dirty_ids
const std::unordered_set< irep_idt > & get_dirty_ids() const
Definition: dirty.h:74
invariant.h
dirtyt::build
void build(const goto_functionst &goto_functions)
Definition: dirty.h:86
dirtyt::dirtyt
dirtyt(const goto_functionst &goto_functions)
Definition: dirty.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
dirtyt::find_dirty
void find_dirty(const exprt &expr)
Definition: dirty.cpp:27
dirtyt::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:37
incremental_dirtyt::dirty_processed_functions
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:133
dirtyt::dirtyt
dirtyt()
Definition: dirty.h:43
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
incremental_dirtyt::populate_dirty_for_function
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:80
dirtyt::dirty
std::unordered_set< irep_idt > dirty
Definition: dirty.h:99
dirtyt::initialized
bool initialized
Definition: dirty.h:36
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
dirtyt::operator()
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:68
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
dirtyt::output
void output(std::ostream &out) const
Definition: dirty.cpp:70
dirtyt::die_if_uninitialized
void die_if_uninitialized() const
Definition: dirty.h:26
incremental_dirtyt::operator()
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:126
goto_functions.h
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
incremental_dirtyt
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:115
std_expr.h
dirtyt::find_dirty_address_of
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:40
validation_modet::INVARIANT
@ INVARIANT