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