cprover
dirty.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Local variables whose address is taken
4 
5 Author: Daniel Kroening
6 
7 Date: March 2013
8 
9 \*******************************************************************/
10 
13 
14 #include "dirty.h"
15 
16 #include <util/std_expr.h>
17 
18 void dirtyt::build(const goto_functiont &goto_function)
19 {
20  forall_goto_program_instructions(it, goto_function.body)
21  {
22  find_dirty(it->code);
23  find_dirty(it->guard);
24  }
25 }
26 
27 void dirtyt::find_dirty(const exprt &expr)
28 {
29  if(expr.id()==ID_address_of)
30  {
31  const address_of_exprt &address_of_expr=to_address_of_expr(expr);
32  find_dirty_address_of(address_of_expr.object());
33  return;
34  }
35 
36  forall_operands(it, expr)
37  find_dirty(*it);
38 }
39 
41 {
42  if(expr.id()==ID_symbol)
43  {
44  const irep_idt &identifier=
46 
47  dirty.insert(identifier);
48  }
49  else if(expr.id()==ID_member)
50  {
51  find_dirty_address_of(to_member_expr(expr).struct_op());
52  }
53  else if(expr.id()==ID_index)
54  {
55  find_dirty_address_of(to_index_expr(expr).array());
56  find_dirty(to_index_expr(expr).index());
57  }
58  else if(expr.id()==ID_dereference)
59  {
60  find_dirty(to_dereference_expr(expr).pointer());
61  }
62  else if(expr.id()==ID_if)
63  {
64  find_dirty_address_of(to_if_expr(expr).true_case());
65  find_dirty_address_of(to_if_expr(expr).false_case());
66  find_dirty(to_if_expr(expr).cond());
67  }
68 }
69 
70 void dirtyt::output(std::ostream &out) const
71 {
73  for(const auto &d : dirty)
74  out << d << '\n';
75 }
76 
81  const irep_idt &id, const goto_functionst::goto_functiont &function)
82 {
83  auto insert_result = dirty_processed_functions.insert(id);
84  if(insert_result.second)
85  dirty.add_function(function);
86 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:80
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:40
exprt & object()
Definition: std_expr.h:3265
Variables whose address is taken.
void die_if_uninitialized() const
Definition: dirty.h:26
const irep_idt & get_identifier() const
Definition: std_expr.h:176
goto_programt body
Definition: goto_function.h:29
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
const irep_idt & id() const
Definition: irep.h:259
void build(const goto_functionst &goto_functions)
Definition: dirty.h:86
API to expression classes.
::goto_functiont goto_functiont
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
#define forall_operands(it, expr)
Definition: expr.h:20
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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:35
Operator to return the address of an object.
Definition: std_expr.h:3255
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
Definition: goto_function.h:26
Base class for all expressions.
Definition: expr.h:54
dirtyt dirty
Definition: dirty.h:132
std::unordered_set< irep_idt > dirty
Definition: dirty.h:99
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:133
void output(std::ostream &out) const
Definition: dirty.cpp:70
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648