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>
21 
22 class dirtyt
23 {
24 public:
25  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
27 
28  explicit dirtyt(const goto_functiont &goto_function)
29  {
30  build(goto_function);
31  }
32 
33  explicit dirtyt(const goto_functionst &goto_functions)
34  {
35  forall_goto_functions(it, goto_functions)
36  build(it->second);
37  }
38 
39  void output(std::ostream &out) const;
40 
41  bool operator()(const irep_idt &id) const
42  {
43  return dirty.find(id)!=dirty.end();
44  }
45 
46  bool operator()(const symbol_exprt &expr) const
47  {
48  return operator()(expr.get_identifier());
49  }
50 
51  const id_sett &get_dirty_ids() const
52  {
53  return dirty;
54  }
55 
56 protected:
57  void build(const goto_functiont &goto_function);
58 
59  // variables whose address is taken
61 
62  void find_dirty(const exprt &expr);
63  void find_dirty_address_of(const exprt &expr);
64 };
65 
66 inline std::ostream &operator<<(
67  std::ostream &out,
68  const dirtyt &dirty)
69 {
70  dirty.output(out);
71  return out;
72 }
73 
74 #endif // CPROVER_ANALYSES_DIRTY_H
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:66
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:40
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Goto Programs with Functions.
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:26
std::unordered_set< irep_idt, irep_id_hash > id_sett
Definition: dirty.h:25
API to expression classes.
bool operator()(const irep_idt &id) const
Definition: dirty.h:41
id_sett dirty
Definition: dirty.h:60
dirtyt(const goto_functionst &goto_functions)
Definition: dirty.h:33
void find_dirty(const exprt &expr)
Definition: dirty.cpp:27
goto_function_templatet< goto_programt > goto_functiont
Base class for all expressions.
Definition: expr.h:46
const id_sett & get_dirty_ids() const
Definition: dirty.h:51
Definition: dirty.h:22
Expression to hold a symbol (variable)
Definition: std_expr.h:82
#define forall_goto_functions(it, functions)
void output(std::ostream &out) const
Definition: dirty.cpp:70
void build(const goto_functiont &goto_function)
Definition: dirty.cpp:18
dirtyt(const goto_functiont &goto_function)
Definition: dirty.h:28
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:46