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 {
72  for(const auto &d : dirty)
73  out << d << '\n';
74 }
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:40
exprt & object()
Definition: std_expr.h:2608
Variables whose address is taken.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:26
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const irep_idt & id() const
Definition: irep.h:189
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
API to expression classes.
id_sett dirty
Definition: dirty.h:60
#define forall_operands(it, expr)
Definition: expr.h:17
void find_dirty(const exprt &expr)
Definition: dirty.cpp:27
Operator to return the address of an object.
Definition: std_expr.h:2593
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void output(std::ostream &out) const
Definition: dirty.cpp:70
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void build(const goto_functiont &goto_function)
Definition: dirty.cpp:18