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