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  forall_goto_functions(it, goto_functions)
94  build(it->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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
dirtyt::operator()
bool operator()(const irep_idt &id) const
Definition: dirty.h:65
incremental_dirtyt::dirty
dirtyt dirty
Definition: dirty.h:135
dirtyt
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
dirtyt::dirtyt
dirtyt(const goto_functiont &goto_function)
Definition: dirty.h:50
operator<<
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:108
invariant.h
dirtyt::add_function
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:83
exprt
Base class for all expressions.
Definition: expr.h:53
incremental_dirtyt::operator()
bool operator()(const irep_idt &id) const
Definition: dirty.h:124
dirtyt::get_dirty_ids
const std::unordered_set< irep_idt > & get_dirty_ids() const
Definition: dirty.h:77
dirtyt::build
void build(const goto_functionst &goto_functions)
Definition: dirty.h:89
dirtyt::dirtyt
dirtyt(const goto_functionst &goto_functions)
Definition: dirty.h:56
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
dirtyt::find_dirty
void find_dirty(const exprt &expr)
Definition: dirty.cpp:24
dirtyt::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:40
incremental_dirtyt::dirty_processed_functions
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:136
dirtyt::dirtyt
dirtyt()
Definition: dirty.h:46
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:77
dirtyt::dirty
std::unordered_set< irep_idt > dirty
Definition: dirty.h:102
dirtyt::initialized
bool initialized
Definition: dirty.h:39
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
dirtyt::operator()
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:71
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
dirtyt::output
void output(std::ostream &out) const
Definition: dirty.cpp:67
dirtyt::die_if_uninitialized
void die_if_uninitialized() const
Definition: dirty.h:29
incremental_dirtyt::operator()
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:129
goto_functions.h
Goto Programs with Functions.
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
incremental_dirtyt
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:119
std_expr.h
API to expression classes.
dirtyt::find_dirty_address_of
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:37
validation_modet::INVARIANT
@ INVARIANT