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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
uninitialized_domaint::has_values
tvt has_values
Definition: uninitialized_domain.h:83
uninitialized_domaint::transform
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...
Definition: uninitialized_domain.cpp:21
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
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:328
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
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:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
uninitialized_domaint::assign
void assign(const exprt &lhs)
Definition: uninitialized_domain.cpp:56
uninitialized_domaint::merge
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
Definition: uninitialized_domain.cpp:81
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:77
uninitialized_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
Definition: uninitialized_domain.cpp:66
symbolt
Symbol table entry.
Definition: symbol.h:28
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:273
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
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:2612
uninitialized_domaint::uninitialized
uninitializedt uninitialized
Definition: uninitialized_domain.h:30
uninitialized_domaint
Definition: uninitialized_domain.h:22
uninitialized_domain.h
Detection for Uninitialized Local Variables.
std_expr.h
API to expression classes.