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  locationt from_l,
62  const irep_idt &function_to,
63  locationt to_l,
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
invariant_set_domaint
Definition: invariant_set_domain.h:21
invariant_set_domaint::merge
bool merge(const invariant_set_domaint &other, locationt, locationt)
Definition: invariant_set_domain.h:36
inv_object_storet
Definition: invariant_set.h:25
invariant_set_domaint::is_top
bool is_top() const override final
Definition: invariant_set_domain.h:85
invariant_set_domaint::make_bottom
void make_bottom() final override
no states
Definition: invariant_set_domain.h:73
threeval.h
invariant_set_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: invariant_set_domain.h:67
invariant_set_domaint::invariant_set_domaint
invariant_set_domaint(value_setst &value_sets, inv_object_storet &object_store, const namespacet &ns)
Definition: invariant_set_domain.h:23
invariant_set_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: invariant_set_domain.h:79
invariant_sett::output
void output(std::ostream &out) const
Definition: invariant_set.cpp:314
tvt::is_known
bool is_known() const
Definition: threeval.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
invariant_set_domaint::has_values
tvt has_values
Definition: invariant_set_domain.h:31
invariant_set_domaint::is_bottom
bool is_bottom() const override final
Definition: invariant_set_domain.h:90
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
invariant_set_domaint::output
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
Definition: invariant_set_domain.h:48
ai.h
Abstract Interpretation.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
tvt
Definition: threeval.h:20
invariant_sett::make_false
void make_false()
Definition: invariant_set.h:122
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition: invariant_set_domain.h:32
value_setst
Definition: value_sets.h:22
invariant_sett
Definition: invariant_set.h:75
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
invariant_sett::make_union
bool make_union(const invariant_sett &other_invariants)
Definition: invariant_set.cpp:886
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
invariant_set.h
Value Set.
tvt::is_true
bool is_true() const
Definition: threeval.h:25
invariant_sett::make_true
void make_true()
Definition: invariant_set.h:114
invariant_set_domaint::transform
virtual void transform(const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l, ai_baset &ai, const namespacet &ns) final override
Definition: invariant_set_domain.cpp:17