-
Notifications
You must be signed in to change notification settings - Fork 300
Expand file tree
/
Copy pathuninitialized_domain.cpp
More file actions
97 lines (77 loc) · 2.12 KB
/
Copy pathuninitialized_domain.cpp
File metadata and controls
97 lines (77 loc) · 2.12 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
/*******************************************************************\
Module: Detection for Uninitialized Local Variables
Author: Daniel Kroening
Date: January 2010
\*******************************************************************/
/// \file
/// Detection for Uninitialized Local Variables
#include "uninitialized_domain.h"
#include <util/std_expr.h>
#include <list>
void uninitialized_domaint::transform(
const irep_idt &,
trace_ptrt trace_from,
const irep_idt &,
trace_ptrt,
ai_baset &,
const namespacet &ns)
{
locationt from{trace_from->current_location()};
if(has_values.is_false())
return;
if(from->is_decl())
{
const irep_idt &identifier = from->decl_symbol().identifier();
const symbolt &symbol = ns.lookup(identifier);
if(!symbol.is_static_lifetime)
uninitialized.insert(identifier);
}
else
{
std::list<exprt> read = expressions_read(*from);
std::list<exprt> written = expressions_written(*from);
for(const auto &expr : written)
assign(expr);
// we only care about the *first* uninitalized use
for(const auto &expr : read)
assign(expr);
}
}
void uninitialized_domaint::assign(const exprt &lhs)
{
if(lhs.id()==ID_index)
assign(to_index_expr(lhs).array());
else if(lhs.id()==ID_member)
assign(to_member_expr(lhs).struct_op());
else if(lhs.id()==ID_symbol)
uninitialized.erase(to_symbol_expr(lhs).identifier());
}
void uninitialized_domaint::output(
std::ostream &out,
const ai_baset &,
const namespacet &) const
{
if(has_values.is_known())
out << has_values.to_string() << '\n';
else
{
for(const auto &id : uninitialized)
out << id << '\n';
}
}
/// \return returns true iff there is something new
bool uninitialized_domaint::merge(
const uninitialized_domaint &other,
trace_ptrt,
trace_ptrt)
{
auto old_uninitialized=uninitialized.size();
uninitialized.insert(
other.uninitialized.begin(),
other.uninitialized.end());
bool changed=
(has_values.is_false() && !other.has_values.is_false()) ||
old_uninitialized!=uninitialized.size();
has_values=tvt::unknown();
return changed;
}