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
33  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
34  final override;
35 
36  void output(
37  std::ostream &out,
38  const ai_baset &ai,
39  const namespacet &ns) const final;
40 
41  void make_top() final override
42  {
43  uninitialized.clear();
44  has_values=tvt(true);
45  }
46 
47  void make_bottom() final override
48  {
49  uninitialized.clear();
50  has_values=tvt(false);
51  }
52 
53  void make_entry() final override
54  {
55  make_top();
56  }
57 
58  bool is_top() const override final
59  {
61  "If domain is top, the uninitialized set must be empty");
62  return has_values.is_true();
63  }
64 
65  bool is_bottom() const override final
66  {
68  "If domain is bottom, the uninitialized set must be empty");
69  return has_values.is_false();
70  }
71 
72  // returns true iff there is something new
73  bool merge(
74  const uninitialized_domaint &other,
75  locationt from,
76  locationt to);
77 
78 private:
80 
81  void assign(const exprt &lhs);
82 };
83 
86 
87 #endif // CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
bool is_false() const
Definition: threeval.h:26
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it.
void make_entry() final override
a reasonable entry-point state
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
ait< uninitialized_domaint > uninitialized_analysist
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::set< irep_idt > uninitializedt
bool is_bottom() const override final
void make_bottom() final override
no states
bool is_true() const
Definition: threeval.h:25
void transform(locationt from, locationt 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...
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
void assign(const exprt &lhs)
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
bool is_top() const override final