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  void insert(const value_ranget &rhs)
42  {
43  for(auto const &value : rhs)
44  insert(value);
45  }
46 
48  {
49  return *begin();
50  }
51 
53  {
54  return values.begin();
55  }
57  {
58  return values.end();
59  }
60 
62  {
63  return values.size();
64  }
65  bool empty() const
66  {
67  return values.empty();
68  }
69 
70  bool operator==(const abstract_object_sett &rhs) const
71  {
72  return values == rhs.values;
73  }
74 
75  void clear()
76  {
77  values.clear();
78  }
79 
80  void
81  output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
82 
86 
87 private:
89 };
90 
92 {
93 public:
94  virtual const abstract_object_sett &get_values() const = 0;
95 };
96 
97 #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_sett::clear
void clear()
Definition: abstract_object_set.h:75
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:52
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:92
abstract_object_sett
Definition: abstract_object_set.h:19
abstract_object_sett::empty
bool empty() const
Definition: abstract_object_set.h:65
abstract_object_sett::end
const_iterator end() const
Definition: abstract_object_set.h:56
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
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
abstract_object_sett::insert
void insert(const value_ranget &rhs)
Definition: abstract_object_set.h:41
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:61
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:47
abstract_object_sett::size_type
value_sett::size_type size_type
Definition: abstract_object_set.h:27
abstract_equalert
Definition: abstract_object.h:476
abstract_hashert
Definition: abstract_object.h:466
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:70
abstract_object_sett::values
value_sett values
Definition: abstract_object_set.h:88
abstract_object_sett::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: abstract_object_set.cpp:23
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
abstract_object_sett::to_interval
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
Definition: abstract_object_set.cpp:40
value_ranget
Definition: abstract_value_object.h:189
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.