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  {
25  }
26 
29 
30  // overloading
31 
32  bool merge(
33  const invariant_set_domaint &other,
34  locationt from,
35  locationt to)
36  {
37  bool changed=invariant_set.make_union(other.invariant_set) ||
38  has_values.is_false();
39  has_values=tvt::unknown();
40 
41  return changed;
42  }
43 
44  void output(
45  std::ostream &out,
46  const ai_baset &ai,
47  const namespacet &ns) const final
48  {
49  if(has_values.is_known())
50  out << has_values.to_string() << '\n';
51  else
52  invariant_set.output("", out);
53  }
54 
55  virtual void transform(
56  locationt from_l,
57  locationt to_l,
58  ai_baset &ai,
59  const namespacet &ns) final;
60 
61  void make_top() final
62  {
63  invariant_set.make_true();
64  has_values=tvt(true);
65  }
66 
67  void make_bottom() final
68  {
69  invariant_set.make_false();
70  has_values=tvt(false);
71  }
72 
73  void make_entry() final
74  {
75  invariant_set.make_true();
76  has_values=tvt(true);
77  }
78 };
79 
80 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
bool is_false() const
Definition: threeval.h:26
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
bool make_union(const invariant_sett &other_invariants)
static tvt unknown()
Definition: threeval.h:33
const char * to_string() const
Definition: threeval.cpp:13
bool merge(const invariant_set_domaint &other, locationt from, locationt to)
bool is_known() const
Definition: threeval.h:28
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Value Set.
virtual void transform(locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final
Abstract Interpretation.
Definition: ai.h:108
goto_programt::const_targett locationt
Definition: ai.h:42
void output(const irep_idt &identifier, std::ostream &out) const