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/pointer_expr.h>
17 #include <util/std_expr.h>
18 
19 void dirtyt::build(const goto_functiont &goto_function)
20 {
21  for(const auto &i : goto_function.body.instructions)
22  i.apply([this](const exprt &e) { find_dirty(e); });
23 }
24 
25 void dirtyt::find_dirty(const exprt &expr)
26 {
27  if(expr.id()==ID_address_of)
28  {
29  const address_of_exprt &address_of_expr=to_address_of_expr(expr);
30  find_dirty_address_of(address_of_expr.object());
31  return;
32  }
33 
34  forall_operands(it, expr)
35  find_dirty(*it);
36 }
37 
39 {
40  if(expr.id()==ID_symbol)
41  {
42  const irep_idt &identifier=
44 
45  dirty.insert(identifier);
46  }
47  else if(expr.id()==ID_member)
48  {
49  find_dirty_address_of(to_member_expr(expr).struct_op());
50  }
51  else if(expr.id()==ID_index)
52  {
53  find_dirty_address_of(to_index_expr(expr).array());
54  find_dirty(to_index_expr(expr).index());
55  }
56  else if(expr.id()==ID_dereference)
57  {
58  find_dirty(to_dereference_expr(expr).pointer());
59  }
60  else if(expr.id()==ID_if)
61  {
62  find_dirty_address_of(to_if_expr(expr).true_case());
63  find_dirty_address_of(to_if_expr(expr).false_case());
64  find_dirty(to_if_expr(expr).cond());
65  }
66 }
67 
68 void dirtyt::output(std::ostream &out) const
69 {
71  for(const auto &d : dirty)
72  out << d << '\n';
73 }
74 
79  const irep_idt &id, const goto_functionst::goto_functiont &function)
80 {
81  auto insert_result = dirty_processed_functions.insert(id);
82  if(insert_result.second)
83  dirty.add_function(function);
84 }
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:83
void build(const goto_functionst &goto_functions)
Definition: dirty.h:89
void find_dirty(const exprt &expr)
Definition: dirty.cpp:25
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:38
void output(std::ostream &out) const
Definition: dirty.cpp:68
std::unordered_set< irep_idt > dirty
Definition: dirty.h:102
void die_if_uninitialized() const
Definition: dirty.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:136
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:78
dirtyt dirty
Definition: dirty.h:135
const irep_idt & id() const
Definition: irep.h:396
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Variables whose address is taken.
#define forall_operands(it, expr)
Definition: expr.h:18
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391