cprover
uninitialized_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Detection for Uninitialized Local Variables
4 
5 Author: Daniel Kroening
6 
7 Date: January 2010
8 
9 \*******************************************************************/
10 
13 
14 #include "uninitialized_domain.h"
15 
16 #include <util/std_expr.h>
17 #include <util/std_code.h>
18 
19 #include <list>
20 
22  const irep_idt &,
23  locationt from,
24  const irep_idt &,
25  locationt,
26  ai_baset &,
27  const namespacet &ns)
28 {
29  if(has_values.is_false())
30  return;
31 
32  if(from->is_decl())
33  {
34  const irep_idt &identifier = to_code_decl(from->code).get_identifier();
35  const symbolt &symbol = ns.lookup(identifier);
36 
37  if(!symbol.is_static_lifetime)
38  uninitialized.insert(identifier);
39  }
40  else
41  {
42  std::list<exprt> read = expressions_read(*from);
43  std::list<exprt> written = expressions_written(*from);
44 
45  for(const auto &expr : written)
46  assign(expr);
47 
48  // we only care about the *first* uninitalized use
49  for(const auto &expr : read)
50  assign(expr);
51  }
52 }
53 
55 {
56  if(lhs.id()==ID_index)
57  assign(to_index_expr(lhs).array());
58  else if(lhs.id()==ID_member)
59  assign(to_member_expr(lhs).struct_op());
60  else if(lhs.id()==ID_symbol)
61  uninitialized.erase(to_symbol_expr(lhs).get_identifier());
62 }
63 
65  std::ostream &out,
66  const ai_baset &,
67  const namespacet &) const
68 {
69  if(has_values.is_known())
70  out << has_values.to_string() << '\n';
71  else
72  {
73  for(const auto &id : uninitialized)
74  out << id << '\n';
75  }
76 }
77 
80  const uninitialized_domaint &other,
81  locationt,
82  locationt)
83 {
84  auto old_uninitialized=uninitialized.size();
85 
86  uninitialized.insert(
87  other.uninitialized.begin(),
88  other.uninitialized.end());
89 
90  bool changed=
91  (has_values.is_false() && !other.has_values.is_false()) ||
92  old_uninitialized!=uninitialized.size();
94 
95  return changed;
96 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
uninitialized_domaint::has_values
tvt has_values
Definition: uninitialized_domain.h:83
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
exprt
Base class for all expressions.
Definition: expr.h:53
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:329
code_declt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:418
tvt::is_known
bool is_known() const
Definition: threeval.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
uninitialized_domaint::assign
void assign(const exprt &lhs)
Definition: uninitialized_domain.cpp:54
uninitialized_domaint::merge
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
Definition: uninitialized_domain.cpp:79
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
tvt::is_false
bool is_false() const
Definition: threeval.h:26
std_code.h
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
uninitialized_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
Definition: uninitialized_domain.cpp:64
symbolt
Symbol table entry.
Definition: symbol.h:28
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:273
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
uninitialized_domaint::uninitialized
uninitializedt uninitialized
Definition: uninitialized_domain.h:30
uninitialized_domaint
Definition: uninitialized_domain.h:22
uninitialized_domain.h
Detection for Uninitialized Local Variables.
std_expr.h
API to expression classes.
uninitialized_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Definition: uninitialized_domain.cpp:21