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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
dirty.h
incremental_dirtyt::dirty
dirtyt dirty
Definition: dirty.h:132
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
dirtyt::add_function
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:80
exprt
Base class for all expressions.
Definition: expr.h:54
dirtyt::build
void build(const goto_functionst &goto_functions)
Definition: dirty.h:86
dirtyt::find_dirty
void find_dirty(const exprt &expr)
Definition: dirty.cpp:27
incremental_dirtyt::dirty_processed_functions
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:133
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:3282
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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:80
dirtyt::dirty
std::unordered_set< irep_idt > dirty
Definition: dirty.h:99
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
dirtyt::output
void output(std::ostream &out) const
Definition: dirty.cpp:70
dirtyt::die_if_uninitialized
void die_if_uninitialized() const
Definition: dirty.h:26
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
std_expr.h
dirtyt::find_dirty_address_of
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:40
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804