Replace definition of value_sett::object_map_dt

src/pointer-analysis/value_set.cpp

@@ -33,7 +33,7 @@ Author: Daniel Kroening, [email protected]
 // 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)

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<object_numberingt::number_type, offsett> 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 <typename It>
-    void insert(It b, It e) { data.insert(b, e); }
-
-    template <typename T>
-    const_iterator find(T &&t) const { return data.find(std::forward<T>(t)); }
+  /// instead of a set of pairs to make lookup by `exprt` easier.
+  using object_map_dt = std::map<object_numberingt::number_type, offsett>;
 
-    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_map_dt> object_mapt;
+  using object_mapt = reference_counting<object_map_dt, empty_object_map>;
 
   /// 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

src/util/reference_counting.h

@@ -14,7 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "invariant.h"
 
-template<typename T>
+/// \tparam empty: pointer to empty data, if unspecified use a reference to
+///   T::blank
+template <typename T, const T &empty = T::blank>
 // 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<class T>
-void reference_counting<T>::remove_ref(dt *old_d)
+template <class T, const T &empty>
+void reference_counting<T, empty>::remove_ref(dt *old_d)
 {
   if(old_d==nullptr)
     return;
@@ -144,8 +146,8 @@ void reference_counting<T>::remove_ref(dt *old_d)
   }
 }
 
-template<class T>
-void reference_counting<T>::detach()
+template <class T, const T &empty>
+void reference_counting<T, empty>::detach()
 {
   #ifdef REFERENCE_COUNTING_DEBUG
   std::cout << "DETACH1: " << d << '\n';
@@ -179,20 +181,20 @@ void reference_counting<T>::detach()
   #endif
 }
 
-template<class T>
+template <class T, const T &empty>
 bool operator==(
-  const reference_counting<T> &o1,
-  const reference_counting<T> &o2)
+  const reference_counting<T, empty> &o1,
+  const reference_counting<T, empty> &o2)
 {
   if(o1.get_d()==o2.get_d())
     return true;
   return o1.read()==o2.read();
 }
 
-template<class T>
+template <class T, const T &empty>
 inline bool operator!=(
-  const reference_counting<T> &i1,
-  const reference_counting<T> &i2)
+  const reference_counting<T, empty> &i1,
+  const reference_counting<T, empty> &i2)
 { return !(i1==i2); }
 
 #endif // CPROVER_UTIL_REFERENCE_COUNTING_H