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 }
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:26
dirty.h
Variables whose address is taken.
incremental_dirtyt::dirty
dirtyt dirty
Definition: dirty.h:135
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
dirtyt::add_function
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:83
exprt
Base class for all expressions.
Definition: expr.h:54
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:25
incremental_dirtyt::dirty_processed_functions
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:136
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:109
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:78
dirtyt::dirty
std::unordered_set< irep_idt > dirty
Definition: dirty.h:102
pointer_expr.h
API to expression classes for Pointers.
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
dirtyt::output
void output(std::ostream &out) const
Definition: dirty.cpp:68
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:2697
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
std_expr.h
API to expression classes.
dirtyt::find_dirty_address_of
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:38