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  locationt from,
23  locationt to,
24  ai_baset &ai,
25  const namespacet &ns)
26 {
27  if(has_values.is_false())
28  return;
29 
30  switch(from->type)
31  {
32  case DECL:
33  {
34  const irep_idt &identifier=
35  to_code_decl(from->code).get_identifier();
36  const symbolt &symbol=ns.lookup(identifier);
37 
38  if(!symbol.is_static_lifetime)
39  uninitialized.insert(identifier);
40  }
41  break;
42 
43  default:
44  {
45  std::list<exprt> read=expressions_read(*from);
46  std::list<exprt> written=expressions_written(*from);
47 
48  for(const auto &expr : written)
49  assign(expr);
50 
51  // we only care about the *first* uninitalized use
52  for(const auto &expr : read)
53  assign(expr);
54  }
55  }
56 }
57 
59 {
60  if(lhs.id()==ID_index)
61  assign(to_index_expr(lhs).array());
62  else if(lhs.id()==ID_member)
64  else if(lhs.id()==ID_symbol)
65  uninitialized.erase(to_symbol_expr(lhs).get_identifier());
66 }
67 
69  std::ostream &out,
70  const ai_baset &ai,
71  const namespacet &ns) const
72 {
73  if(has_values.is_known())
74  out << has_values.to_string() << '\n';
75  else
76  {
77  for(const auto &id : uninitialized)
78  out << id << '\n';
79  }
80 }
81 
84  const uninitialized_domaint &other,
85  locationt from,
86  locationt to)
87 {
88  auto old_uninitialized=uninitialized.size();
89 
90  uninitialized.insert(
91  other.uninitialized.begin(),
92  other.uninitialized.end());
93 
94  bool changed=
95  (has_values.is_false() && !other.has_values.is_false()) ||
96  old_uninitialized!=uninitialized.size();
98 
99  return changed;
100 }
bool is_false() const
Definition: threeval.h:26
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
static tvt unknown()
Definition: threeval.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool is_static_lifetime
Definition: symbol.h:67
const char * to_string() const
Definition: threeval.cpp:13
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
const irep_idt & id() const
Definition: irep.h:189
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.
const irep_idt & get_identifier() const
Definition: std_code.cpp:14
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Detection for Uninitialized Local Variables.
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3911
void assign(const exprt &lhs)
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
goto_programt::const_targett locationt
Definition: ai.h:44
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130