cprover
uninitialized_domain.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Detection for Uninitialized Local Variables
4
5Author: Daniel Kroening
6
7Date: 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{
23public:
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 trace_ptrt trace_from,
35 const irep_idt &function_to,
36 trace_ptrt trace_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
78 merge(const uninitialized_domaint &other, trace_ptrt from, trace_ptrt to);
79
80private:
82
83 void assign(const exprt &lhs);
84};
85
88
89#endif // CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Definition: threeval.h:20
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
void assign(const exprt &lhs)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
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...
std::set< irep_idt > uninitializedt
bool is_top() const override final
bool is_bottom() const override final
bool merge(const uninitialized_domaint &other, trace_ptrt from, trace_ptrt to)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void make_entry() final override
Make this domain a reasonable entry-point state.
void make_bottom() final override
no states
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
ait< uninitialized_domaint > uninitialized_analysist