CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 {
23 if(i.is_other())
24 {
25 search_other(i);
26 }
27 else
28 {
29 i.apply([this](const exprt &e) { find_dirty(e); });
30 }
31 }
32}
33
35{
36 INVARIANT(instruction.is_other(), "instruction type must be OTHER");
37 if(instruction.get_other().id() == ID_code)
38 {
39 const codet &code = instruction.get_other();
40 const irep_idt &statement = code.get_statement();
41 if(
42 statement == ID_expression || statement == ID_array_set ||
43 statement == ID_array_equal || statement == ID_array_copy ||
44 statement == ID_array_replace || statement == ID_havoc_object ||
45 statement == ID_input || statement == ID_output)
46 {
47 for(const auto &op : code.operands())
48 find_dirty(op);
49 }
50 // other possible cases according to goto_programt::instructiont::output
51 // and goto_symext::symex_other:
52 // statement == ID_fence ||
53 // statement == ID_user_specified_predicate ||
54 // statement == ID_user_specified_parameter_predicates ||
55 // statement == ID_user_specified_return_predicates ||
56 // statement == ID_decl || statement == ID_nondet || statement == ID_asm)
57 }
58}
59
60void dirtyt::find_dirty(const exprt &expr)
61{
62 if(expr.id() == ID_address_of)
63 {
66 return;
67 }
68
69 for(const auto &op : expr.operands())
70 find_dirty(op);
71}
72
74{
75 if(expr.id() == ID_symbol)
76 {
77 const irep_idt &identifier = to_symbol_expr(expr).get_identifier();
78
79 dirty.insert(identifier);
80 }
81 else if(expr.id() == ID_member)
82 {
83 find_dirty_address_of(to_member_expr(expr).struct_op());
84 }
85 else if(expr.id() == ID_index)
86 {
88 find_dirty(to_index_expr(expr).index());
89 }
90 else if(expr.id() == ID_dereference)
91 {
92 find_dirty(to_dereference_expr(expr).pointer());
93 }
94 else if(expr.id() == ID_if)
95 {
96 find_dirty_address_of(to_if_expr(expr).true_case());
97 find_dirty_address_of(to_if_expr(expr).false_case());
98 find_dirty(to_if_expr(expr).cond());
99 }
100}
101
102void dirtyt::output(std::ostream &out) const
103{
105 for(const auto &d : dirty)
106 out << d << '\n';
107}
108
113 const irep_idt &id,
114 const goto_functionst::goto_functiont &function)
115{
117 if(insert_result.second)
118 dirty.add_function(function);
119}
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
void add_function(const goto_functiont &goto_function)
Definition dirty.h:84
void build(const goto_functionst &goto_functions)
Definition dirty.h:90
void find_dirty(const exprt &expr)
Definition dirty.cpp:60
void find_dirty_address_of(const exprt &expr)
Definition dirty.cpp:73
void output(std::ostream &out) const
Definition dirty.cpp:102
std::unordered_set< irep_idt > dirty
Definition dirty.h:103
void search_other(const goto_programt::instructiont &instruction)
Definition dirty.cpp:34
void die_if_uninitialized() const
Definition dirty.h:30
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
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:112
const irep_idt & id() const
Definition irep.h:388
Variables whose address is taken.
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272