diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 352fdab1c50..be9edde81c7 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -33,7 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com // Due to a large number of functions defined inline, `value_sett` and // associated types are documented in its header file, `value_set.h`. -const value_sett::object_map_dt value_sett::object_map_dt::blank{}; +const value_sett::object_map_dt value_sett::empty_object_map{}; object_numberingt value_sett::object_numbering; bool value_sett::field_sensitive(const irep_idt &id, const typet &type) diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index ec040df7499..23af996dab3 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -89,73 +89,10 @@ class value_sett /// offsets (`offsett` instances). This is the RHS set of a single row of /// the enclosing `value_sett`, such as `{ null, dynamic_object1 }`. /// The set is represented as a map from numbered `exprt`s to `offsett` - /// instead of a set of pairs to make lookup by `exprt` easier. All - /// methods matching the interface of `std::map` forward those methods - /// to the internal map. - class object_map_dt - { - typedef std::map data_typet; - data_typet data; - - public: - // NOLINTNEXTLINE(readability/identifiers) - typedef data_typet::iterator iterator; - // NOLINTNEXTLINE(readability/identifiers) - typedef data_typet::const_iterator const_iterator; - // NOLINTNEXTLINE(readability/identifiers) - typedef data_typet::value_type value_type; - // NOLINTNEXTLINE(readability/identifiers) - typedef data_typet::key_type key_type; - - iterator begin() { return data.begin(); } - const_iterator begin() const { return data.begin(); } - const_iterator cbegin() const { return data.cbegin(); } - - iterator end() { return data.end(); } - const_iterator end() const { return data.end(); } - const_iterator cend() const { return data.cend(); } - - size_t size() const { return data.size(); } - bool empty() const { return data.empty(); } - - void erase(key_type i) { data.erase(i); } - void erase(const_iterator it) { data.erase(it); } - - offsett &operator[](key_type i) - { - return data[i]; - } - offsett &at(key_type i) - { - return data.at(i); - } - const offsett &at(key_type i) const - { - return data.at(i); - } - - template - void insert(It b, It e) { data.insert(b, e); } - - template - const_iterator find(T &&t) const { return data.find(std::forward(t)); } + /// instead of a set of pairs to make lookup by `exprt` easier. + using object_map_dt = std::map; - static const object_map_dt blank; - - object_map_dt()=default; - - bool operator==(const object_map_dt &other) const - { - return data==other.data; - } - bool operator!=(const object_map_dt &other) const - { - return !(*this==other); - } - - protected: - ~object_map_dt()=default; - }; + static const object_map_dt empty_object_map; /// Converts an `object_map_dt` element `object_number -> offset` into an /// `object_descriptor_exprt` with @@ -175,7 +112,7 @@ class value_sett /// /// Then the set { dynamic_object1 }, represented by an `object_map_dt`, can /// be shared between the two `value_sett` instances. - typedef reference_counting object_mapt; + using object_mapt = reference_counting; /// Sets an element in object map `dest` to match an existing element `it` /// from a different map. Any existing element for the same `exprt` is diff --git a/src/util/reference_counting.h b/src/util/reference_counting.h index 9694fdcbdcb..dc6118598fb 100644 --- a/src/util/reference_counting.h +++ b/src/util/reference_counting.h @@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" -template +/// \tparam empty: pointer to empty data, if unspecified use a reference to +/// T::blank +template // NOLINTNEXTLINE(readability/identifiers) class reference_counting { @@ -67,7 +69,7 @@ class reference_counting const T &read() const { if(d==nullptr) - return T::blank; + return empty; return *d; } @@ -115,8 +117,8 @@ class reference_counting } }; -template -void reference_counting::remove_ref(dt *old_d) +template +void reference_counting::remove_ref(dt *old_d) { if(old_d==nullptr) return; @@ -144,8 +146,8 @@ void reference_counting::remove_ref(dt *old_d) } } -template -void reference_counting::detach() +template +void reference_counting::detach() { #ifdef REFERENCE_COUNTING_DEBUG std::cout << "DETACH1: " << d << '\n'; @@ -179,20 +181,20 @@ void reference_counting::detach() #endif } -template +template bool operator==( - const reference_counting &o1, - const reference_counting &o2) + const reference_counting &o1, + const reference_counting &o2) { if(o1.get_d()==o2.get_d()) return true; return o1.read()==o2.read(); } -template +template inline bool operator!=( - const reference_counting &i1, - const reference_counting &i2) + const reference_counting &i1, + const reference_counting &i2) { return !(i1==i2); } #endif // CPROVER_UTIL_REFERENCE_COUNTING_H