cprover
abstract_object_set.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Jez Higgins, jez@jezuk.co.uk
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CBMC_ABSTRACT_OBJECT_SET_H
13 #define CBMC_ABSTRACT_OBJECT_SET_H
14 
16 #include <unordered_set>
17 
19 {
20 public:
21  using value_sett = std::unordered_set<
25  using const_iterator = value_sett::const_iterator;
26  using value_type = value_sett::value_type;
28 
30  {
31  values.insert(o);
32  }
34  {
35  values.insert(std::move(o));
36  }
37  void insert(const abstract_object_sett &rhs)
38  {
39  values.insert(rhs.begin(), rhs.end());
40  }
41 
43  {
44  return *begin();
45  }
46 
48  {
49  return values.begin();
50  }
52  {
53  return values.end();
54  }
55 
57  {
58  return values.size();
59  }
60  bool empty() const
61  {
62  return values.empty();
63  }
64 
65  bool operator==(const abstract_object_sett &rhs) const
66  {
67  return values == rhs.values;
68  }
69 
70  void
71  output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
72 
73 private:
75 };
76 
78 {
79 public:
80  virtual const abstract_object_sett &get_values() const = 0;
81 };
82 
83 #endif //CBMC_ABSTRACT_OBJECT_SET_H
abstract_object_sett::insert
void insert(const abstract_object_sett &rhs)
Definition: abstract_object_set.h:37
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_object_sett::begin
const_iterator begin() const
Definition: abstract_object_set.h:47
abstract_object_sett::value_sett
std::unordered_set< abstract_object_pointert, abstract_hashert, abstract_equalert > value_sett
Definition: abstract_object_set.h:24
value_set_tag
Definition: abstract_object_set.h:78
abstract_object_sett
Definition: abstract_object_set.h:19
abstract_object_sett::empty
bool empty() const
Definition: abstract_object_set.h:60
abstract_object_sett::end
const_iterator end() const
Definition: abstract_object_set.h:51
abstract_object_sett::const_iterator
value_sett::const_iterator const_iterator
Definition: abstract_object_set.h:25
abstract_object_sett::insert
void insert(abstract_object_pointert &&o)
Definition: abstract_object_set.h:33
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_object_sett::size
value_sett::size_type size() const
Definition: abstract_object_set.h:56
abstract_object_sett::value_type
value_sett::value_type value_type
Definition: abstract_object_set.h:26
value_set_tag::get_values
virtual const abstract_object_sett & get_values() const =0
abstract_object_sett::insert
void insert(const abstract_object_pointert &o)
Definition: abstract_object_set.h:29
abstract_object_sett::first
abstract_object_pointert first() const
Definition: abstract_object_set.h:42
abstract_object_sett::size_type
value_sett::size_type size_type
Definition: abstract_object_set.h:27
abstract_equalert
Definition: abstract_object.h:472
abstract_hashert
Definition: abstract_object.h:462
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_object_sett::operator==
bool operator==(const abstract_object_sett &rhs) const
Definition: abstract_object_set.h:65
abstract_object_sett::values
value_sett values
Definition: abstract_object_set.h:74
abstract_object_sett::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: abstract_object_set.cpp:21
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.