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  switch(from->type)
33  {
34  case DECL:
35  {
36  const irep_idt &identifier=
37  to_code_decl(from->code).get_identifier();
38  const symbolt &symbol=ns.lookup(identifier);
39 
40  if(!symbol.is_static_lifetime)
41  uninitialized.insert(identifier);
42  }
43  break;
44 
45  default:
46  {
47  std::list<exprt> read=expressions_read(*from);
48  std::list<exprt> written=expressions_written(*from);
49 
50  for(const auto &expr : written)
51  assign(expr);
52 
53  // we only care about the *first* uninitalized use
54  for(const auto &expr : read)
55  assign(expr);
56  }
57  }
58 }
59 
61 {
62  if(lhs.id()==ID_index)
63  assign(to_index_expr(lhs).array());
64  else if(lhs.id()==ID_member)
66  else if(lhs.id()==ID_symbol)
67  uninitialized.erase(to_symbol_expr(lhs).get_identifier());
68 }
69 
71  std::ostream &out,
72  const ai_baset &,
73  const namespacet &) const
74 {
75  if(has_values.is_known())
76  out << has_values.to_string() << '\n';
77  else
78  {
79  for(const auto &id : uninitialized)
80  out << id << '\n';
81  }
82 }
83 
86  const uninitialized_domaint &other,
87  locationt,
88  locationt)
89 {
90  auto old_uninitialized=uninitialized.size();
91 
92  uninitialized.insert(
93  other.uninitialized.begin(),
94  other.uninitialized.end());
95 
96  bool changed=
97  (has_values.is_false() && !other.has_values.is_false()) ||
98  old_uninitialized!=uninitialized.size();
100 
101  return changed;
102 }
bool is_false() const
Definition: threeval.h:26
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
const irep_idt & get_identifier() const
Definition: std_code.h:370
static tvt unknown()
Definition: threeval.h:33
Symbol table entry.
Definition: symbol.h:27
bool is_static_lifetime
Definition: symbol.h:65
const char * to_string() const
Definition: threeval.cpp:13
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt 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...
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
const irep_idt & id() const
Definition: irep.h:259
bool is_known() const
Definition: threeval.h:28
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Detection for Uninitialized Local Variables.
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3931
void assign(const exprt &lhs)
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
exprt & array()
Definition: std_expr.h:1621
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166