cprover
invariant_set_domain.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
13 #define CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
14 
15 #include <util/threeval.h>
16 
17 #include "ai.h"
18 #include "invariant_set.h"
19 
21 {
22 public:
24  value_setst &value_sets,
25  inv_object_storet &object_store,
26  const namespacet &ns)
27  : has_values(false), invariant_set(value_sets, object_store, ns)
28  {
29  }
30 
33 
34  // overloading
35 
36  bool merge(
37  const invariant_set_domaint &other,
38  locationt,
39  locationt)
40  {
41  bool changed=invariant_set.make_union(other.invariant_set) ||
44 
45  return changed;
46  }
47 
48  void output(
49  std::ostream &out,
50  const ai_baset &,
51  const namespacet &) const final override
52  {
53  if(has_values.is_known())
54  out << has_values.to_string() << '\n';
55  else
56  invariant_set.output(out);
57  }
58 
59  virtual void transform(
60  const irep_idt &function_from,
61  trace_ptrt trace_from,
62  const irep_idt &function_to,
63  trace_ptrt trace_to,
64  ai_baset &ai,
65  const namespacet &ns) final override;
66 
67  void make_top() final override
68  {
70  has_values=tvt(true);
71  }
72 
73  void make_bottom() final override
74  {
76  has_values=tvt(false);
77  }
78 
79  void make_entry() final override
80  {
82  has_values=tvt(true);
83  }
84 
85  bool is_top() const override final
86  {
87  return has_values.is_true();
88  }
89 
90  bool is_bottom() const override final
91  {
92  return has_values.is_false();
93  }
94 };
95 
96 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::const_targett locationt
Definition: ai_domain.h:77
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
bool is_bottom() const override final
bool merge(const invariant_set_domaint &other, locationt, locationt)
void make_entry() final override
Make this domain a reasonable entry-point state.
bool is_top() const override final
void make_bottom() final override
no states
invariant_set_domaint(value_setst &value_sets, inv_object_storet &object_store, const namespacet &ns)
virtual 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...
void output(std::ostream &out) const
bool make_union(const invariant_sett &other_invariants)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Definition: threeval.h:20
bool is_known() const
Definition: threeval.h:28
const char * to_string() const
Definition: threeval.cpp:13
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
static tvt unknown()
Definition: threeval.h:33
Value Set.