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,
35  locationt)
36  {
37  bool changed=invariant_set.make_union(other.invariant_set) ||
40 
41  return changed;
42  }
43 
44  void output(
45  std::ostream &out,
46  const ai_baset &,
47  const namespacet &) const final override
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  const irep_idt &function_from,
57  locationt from_l,
58  const irep_idt &function_to,
59  locationt to_l,
60  ai_baset &ai,
61  const namespacet &ns) final override;
62 
63  void make_top() final override
64  {
66  has_values=tvt(true);
67  }
68 
69  void make_bottom() final override
70  {
72  has_values=tvt(false);
73  }
74 
75  void make_entry() final override
76  {
78  has_values=tvt(true);
79  }
80 
81  bool is_top() const override final
82  {
83  return has_values.is_true();
84  }
85 
86  bool is_bottom() const override final
87  {
88  return has_values.is_false();
89  }
90 };
91 
92 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
bool is_false() const
Definition: threeval.h:26
bool make_union(const invariant_sett &other_invariants)
void make_bottom() final override
no states
static tvt unknown()
Definition: threeval.h:33
void make_entry() final override
Make this domain a reasonable entry-point state.
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it...
const char * to_string() const
Definition: threeval.cpp:13
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
bool is_known() const
Definition: threeval.h:28
Definition: threeval.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Value Set.
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool is_bottom() const override final
bool is_true() const
Definition: threeval.h:25
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
goto_programt::const_targett locationt
Definition: ai_domain.h:40
bool merge(const invariant_set_domaint &other, locationt, locationt)
void output(const irep_idt &identifier, std::ostream &out) const
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
how function calls are treated: a) there is an edge from each call site to the function head b) there...
bool is_top() const override final