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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:399
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
exprt
Base class for all expressions.
Definition: expr.h:54
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:311
code_declt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:370
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:93
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
uninitialized_domaint::assign
void assign(const exprt &lhs)
Definition: uninitialized_domain.cpp:60
uninitialized_domaint::merge
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
Definition: uninitialized_domain.cpp:85
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3931
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:40
uninitialized_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
Definition: uninitialized_domain.cpp:70
DECL
Definition: goto_program.h:47
symbolt
Symbol table entry.
Definition: symbol.h:27
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:266
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
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:3959
uninitialized_domaint::uninitialized
uninitializedt uninitialized
Definition: uninitialized_domain.h:30
uninitialized_domaint
Definition: uninitialized_domain.h:21
uninitialized_domain.h
std_expr.h
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
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Definition: uninitialized_domain.cpp:21