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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
invariant_set_domaint
Definition: invariant_set_domain.h:20
invariant_set_domaint::merge
bool merge(const invariant_set_domaint &other, locationt, locationt)
Definition: invariant_set_domain.h:32
invariant_set_domaint::is_top
bool is_top() const override final
Definition: invariant_set_domain.h:81
invariant_set_domaint::make_bottom
void make_bottom() final override
no states
Definition: invariant_set_domain.h:69
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:63
invariant_set_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: invariant_set_domain.h:75
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:93
invariant_set_domaint::has_values
tvt has_values
Definition: invariant_set_domain.h:27
invariant_sett::output
void output(const irep_idt &identifier, std::ostream &out) const
Definition: invariant_set.cpp:317
invariant_set_domaint::is_bottom
bool is_bottom() const override final
Definition: invariant_set_domain.h:86
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:44
ai.h
tvt::is_false
bool is_false() const
Definition: threeval.h:26
tvt
Definition: threeval.h:19
invariant_sett::make_false
void make_false()
Definition: invariant_set.h:124
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:40
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition: invariant_set_domain.h:28
invariant_sett
Definition: invariant_set.h:77
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
invariant_sett::make_union
bool make_union(const invariant_sett &other_invariants)
Definition: invariant_set.cpp:902
invariant_set_domaint::invariant_set_domaint
invariant_set_domaint()
Definition: invariant_set_domain.h:23
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
invariant_set.h
tvt::is_true
bool is_true() const
Definition: threeval.h:25
invariant_sett::make_true
void make_true()
Definition: invariant_set.h:116
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
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Definition: invariant_set_domain.cpp:17