CBMC
Loading...
Searching...
No Matches
uninitialized_domain.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Detection for Uninitialized Local Variables
4
5Author: Daniel Kroening
6
7Date: January 2010
8
9\*******************************************************************/
10
13
15
16#include <util/std_expr.h>
17
18#include <list>
19
21 const irep_idt &,
23 const irep_idt &,
25 ai_baset &,
26 const namespacet &ns)
27{
28 locationt from{trace_from->current_location()};
29
31 return;
32
33 if(from->is_decl())
34 {
35 const irep_idt &identifier = from->decl_symbol().get_identifier();
36 const symbolt &symbol = ns.lookup(identifier);
37
38 if(!symbol.is_static_lifetime)
39 uninitialized.insert(identifier);
40 }
41 else
42 {
43 std::list<exprt> read = expressions_read(*from);
44 std::list<exprt> written = expressions_written(*from);
45
46 for(const auto &expr : written)
47 assign(expr);
48
49 // we only care about the *first* uninitalized use
50 for(const auto &expr : read)
51 assign(expr);
52 }
53}
54
56{
57 if(lhs.id()==ID_index)
58 assign(to_index_expr(lhs).array());
59 else if(lhs.id()==ID_member)
60 assign(to_member_expr(lhs).struct_op());
61 else if(lhs.id()==ID_symbol)
62 uninitialized.erase(to_symbol_expr(lhs).get_identifier());
63}
64
66 std::ostream &out,
67 const ai_baset &,
68 const namespacet &) const
69{
71 out << has_values.to_string() << '\n';
72 else
73 {
74 for(const auto &id : uninitialized)
75 out << id << '\n';
76 }
77}
78
81 const uninitialized_domaint &other,
84{
86
87 uninitialized.insert(
88 other.uninitialized.begin(),
89 other.uninitialized.end());
90
91 bool changed=
92 (has_values.is_false() && !other.has_values.is_false()) ||
95
96 return changed;
97}
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
bool is_known() const
Definition threeval.h:28
const char * to_string() const
Definition threeval.cpp:13
bool is_false() const
Definition threeval.h:26
static tvt unknown()
Definition threeval.h:33
void assign(const exprt &lhs)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
bool merge(const uninitialized_domaint &other, trace_ptrt from, trace_ptrt to)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
Detection for Uninitialized Local Variables.