cprover
dirty.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Local variables whose address is taken
4
5Author: Daniel Kroening
6
7Date: March 2013
8
9\*******************************************************************/
10
13
14#include "dirty.h"
15
16#include <util/pointer_expr.h>
17#include <util/std_expr.h>
18
19void 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
25void 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 {
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
68void 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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189