cprover
Loading...
Searching...
No Matches
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.
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...
goto_programt body
instructionst instructions
The list of instructions in the goto program.
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
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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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