cprover
uninitialized_domain.h
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 #ifndef CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
15 #define CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
16 
17 #include <util/threeval.h>
18 
19 #include "ai.h"
20 
22 {
23 public:
25  {
26  }
27 
28  // Locals that are declared but may not be initialized
29  typedef std::set<irep_idt> uninitializedt;
31 
32  void transform(
33  const irep_idt &function_from,
34  locationt from,
35  const irep_idt &function_to,
36  locationt to,
37  ai_baset &ai,
38  const namespacet &ns) final override;
39 
40  void output(
41  std::ostream &out,
42  const ai_baset &ai,
43  const namespacet &ns) const final;
44 
45  void make_top() final override
46  {
47  uninitialized.clear();
48  has_values=tvt(true);
49  }
50 
51  void make_bottom() final override
52  {
53  uninitialized.clear();
54  has_values=tvt(false);
55  }
56 
57  void make_entry() final override
58  {
59  make_top();
60  }
61 
62  bool is_top() const override final
63  {
65  "If domain is top, the uninitialized set must be empty");
66  return has_values.is_true();
67  }
68 
69  bool is_bottom() const override final
70  {
72  "If domain is bottom, the uninitialized set must be empty");
73  return has_values.is_false();
74  }
75 
76  // returns true iff there is something new
77  bool merge(
78  const uninitialized_domaint &other,
79  locationt from,
80  locationt to);
81 
82 private:
84 
85  void assign(const exprt &lhs);
86 };
87 
90 
91 #endif // CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
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
threeval.h
uninitialized_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: uninitialized_domain.h:45
exprt
Base class for all expressions.
Definition: expr.h:53
ait< uninitialized_domaint >
uninitialized_analysist
ait< uninitialized_domaint > uninitialized_analysist
Definition: uninitialized_domain.h:89
uninitialized_domaint::is_bottom
bool is_bottom() const override final
Definition: uninitialized_domain.h:69
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
uninitialized_domaint::assign
void assign(const exprt &lhs)
Definition: uninitialized_domain.cpp:54
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
uninitialized_domaint::merge
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
Definition: uninitialized_domain.cpp:79
ai.h
Abstract Interpretation.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
tvt
Definition: threeval.h:20
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
uninitialized_domaint::uninitialized_domaint
uninitialized_domaint()
Definition: uninitialized_domain.h:24
uninitialized_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
Definition: uninitialized_domain.cpp:64
uninitialized_domaint::is_top
bool is_top() const override final
Definition: uninitialized_domain.h:62
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
uninitialized_domaint::uninitialized
uninitializedt uninitialized
Definition: uninitialized_domain.h:30
uninitialized_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: uninitialized_domain.h:57
uninitialized_domaint::make_bottom
void make_bottom() final override
no states
Definition: uninitialized_domain.h:51
uninitialized_domaint
Definition: uninitialized_domain.h:22
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
tvt::is_true
bool is_true() const
Definition: threeval.h:25
uninitialized_domaint::uninitializedt
std::set< irep_idt > uninitializedt
Definition: uninitialized_domain.h:29
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
Definition: uninitialized_domain.cpp:21