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  locationt from,
34  locationt to,
35  ai_baset &ai,
36  const namespacet &ns) final;
37 
38  void output(
39  std::ostream &out,
40  const ai_baset &ai,
41  const namespacet &ns) const final;
42 
43  void make_top() final
44  {
45  uninitialized.clear();
46  has_values=tvt(true);
47  }
48 
49  void make_bottom() final
50  {
51  uninitialized.clear();
52  has_values=tvt(false);
53  }
54 
55  void make_entry() final
56  {
57  make_top();
58  }
59 
60  // returns true iff there is something new
61  bool merge(
62  const uninitialized_domaint &other,
63  locationt from,
64  locationt to);
65 
66 private:
68 
69  void assign(const exprt &lhs);
70 };
71 
74 
75 #endif // CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
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:62
std::set< irep_idt > uninitializedt
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
Abstract Interpretation.
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
void assign(const exprt &lhs)
bool merge(const uninitialized_domaint &other, locationt from, locationt to)
goto_programt::const_targett locationt
Definition: ai.h:42