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 
20  locationt from,
21  locationt to,
22  ai_baset &ai,
23  const namespacet &ns)
24 {
25  if(has_values.is_false())
26  return;
27 
28  switch(from->type)
29  {
30  case DECL:
31  {
32  const irep_idt &identifier=
33  to_code_decl(from->code).get_identifier();
34  const symbolt &symbol=ns.lookup(identifier);
35 
36  if(!symbol.is_static_lifetime)
37  uninitialized.insert(identifier);
38  }
39  break;
40 
41  default:
42  {
43  std::list<exprt> read=expressions_read(*from);
44  std::list<exprt> written=expressions_written(*from);
45 
46  forall_expr_list(it, written) assign(*it);
47 
48  // we only care about the *first* uninitalized use
49  forall_expr_list(it, read) assign(*it);
50  }
51  }
52 }
53 
55 {
56  if(lhs.id()==ID_index)
57  assign(to_index_expr(lhs).array());
58  else if(lhs.id()==ID_member)
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 &ai,
67  const namespacet &ns) 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 from,
82  locationt to)
83 {
84  unsigned 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 }
bool is_false() const
Definition: threeval.h:26
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
static tvt unknown()
Definition: threeval.h:33
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
const char * to_string() const
Definition: threeval.cpp:13
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
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:62
#define forall_expr_list(it, expr)
Definition: expr.h:36
Detection for Uninitialized Local Variables.
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void assign(const exprt &lhs)
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
goto_programt::const_targett locationt
Definition: ai.h:42
exprt & array()
Definition: std_expr.h:1198