From 377b1600e178eb6a62cc55fc8732988746c0b9d6 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 11:04:06 +0100
Subject: [PATCH 01/14] Remove inheritance from std containers in goto_rw.h

---
 src/analyses/goto_rw.h | 58 ++++++++++++++++++++++++++++++++++++------
 1 file changed, 50 insertions(+), 8 deletions(-)

diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index 1f92c3e0e14..e53945243c0 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -44,6 +44,14 @@ void goto_rw(const goto_functionst &goto_functions,
 class range_domain_baset
 {
 public:
+  range_domain_baset()=default;
+
+  range_domain_baset(const range_domain_baset &rhs)=delete;
+  range_domain_baset &operator=(const range_domain_baset &rhs)=delete;
+
+  range_domain_baset(range_domain_baset &&rhs)=delete;
+  range_domain_baset &operator=(range_domain_baset &&rhs)=delete;
+
   virtual ~range_domain_baset();
 
   virtual void output(const namespacet &ns, std::ostream &out) const=0;
@@ -61,12 +69,29 @@ inline range_spect to_range_spect(const mp_integer &size)
 }
 
 // each element x represents a range of bits [x.first, x.second.first)
-class range_domaint:
-  public range_domain_baset,
-  public std::list<std::pair<range_spect, range_spect> >
+class range_domaint:public range_domain_baset
 {
+  typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
+  sub_typet data;
+
 public:
-  virtual void output(const namespacet &ns, std::ostream &out) const;
+  void output(const namespacet &ns, std::ostream &out) const override;
+
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef sub_typet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef sub_typet::const_iterator const_iterator;
+
+  iterator begin() { return data.begin(); }
+  const_iterator begin() const { return data.begin(); }
+  const_iterator cbegin() const { return data.begin(); }
+
+  iterator end() { return data.end(); }
+  const_iterator end() const { return data.end(); }
+  const_iterator cend() const { return data.end(); }
+
+  template <typename T>
+  void push_back(T &&v) { data.push_back(std::forward<T>(v)); }
 };
 
 class array_exprt;
@@ -257,12 +282,29 @@ class rw_range_set_value_sett:public rw_range_sett
     const range_spect &size);
 };
 
-class guarded_range_domaint:
-  public range_domain_baset,
-  public std::multimap<range_spect, std::pair<range_spect, exprt> >
+class guarded_range_domaint:public range_domain_baset
 {
+  typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
+  sub_typet data;
+
 public:
-  virtual void output(const namespacet &ns, std::ostream &out) const;
+  virtual void output(const namespacet &ns, std::ostream &out) const override;
+
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef sub_typet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef sub_typet::const_iterator const_iterator;
+
+  iterator begin() { return data.begin(); }
+  const_iterator begin() const { return data.begin(); }
+  const_iterator cbegin() const { return data.begin(); }
+
+  iterator end() { return data.end(); }
+  const_iterator end() const { return data.end(); }
+  const_iterator cend() const { return data.end(); }
+
+  template<typename T>
+  iterator insert(T &&v) { return data.insert(std::forward<T>(v)); }
 };
 
 class rw_guarded_range_set_value_sett:public rw_range_set_value_sett

From ed2640d5839632e492eb3f375f4aa71be0611520 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 11:48:41 +0100
Subject: [PATCH 02/14] Remove inheritance from list in data_dp.h

---
 src/goto-instrument/wmm/data_dp.cpp | 44 ++++++++++++++---------------
 src/goto-instrument/wmm/data_dp.h   |  6 ++--
 2 files changed, 26 insertions(+), 24 deletions(-)

diff --git a/src/goto-instrument/wmm/data_dp.cpp b/src/goto-instrument/wmm/data_dp.cpp
index d24b17d9651..c9baff90f95 100644
--- a/src/goto-instrument/wmm/data_dp.cpp
+++ b/src/goto-instrument/wmm/data_dp.cpp
@@ -24,13 +24,13 @@ void data_dpt::dp_analysis(
   const datat &write,
   bool local_write)
 {
-  const_iterator it;
+  data_typet::const_iterator it;
 
-  for(it=begin(); it!=end(); ++it)
+  for(it=data.cbegin(); it!=data.cend(); ++it)
   {
     if(local_read && it->id==read.id)
     {
-      insert(
+      data.insert(
         datat(
           write.id,
           (local_write?source_locationt():write.loc),
@@ -40,7 +40,7 @@ void data_dpt::dp_analysis(
 
     if(local_write && it->id==write.id)
     {
-      insert(
+      data.insert(
         datat(
           read.id,
           (local_read?source_locationt():read.loc),
@@ -49,12 +49,12 @@ void data_dpt::dp_analysis(
     }
   }
 
-  if(it==end())
+  if(it==data.cend())
   {
     ++class_nb;
-    insert(
+    data.insert(
       datat(read.id, (local_read?source_locationt():read.loc), class_nb));
-    insert(
+    data.insert(
       datat(write.id, (local_write?source_locationt():write.loc), class_nb));
   }
 }
@@ -71,11 +71,11 @@ void data_dpt::dp_analysis(
 /// search in N^2
 bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
 {
-  for(const_iterator it1=begin(); it1!=end(); ++it1)
+  for(auto it1=data.cbegin(); it1!=data.cend(); ++it1)
   {
-    const_iterator it2=it1;
+    auto it2=it1;
     ++it2;
-    if(it2==end())
+    if(it2==data.cend())
       break;
 
     if(e1.local)
@@ -89,7 +89,7 @@ bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
         continue;
     }
 
-    for(; it2!=end(); ++it2)
+    for(; it2!=data.cend(); ++it2)
     {
       if(e2.local)
       {
@@ -116,42 +116,42 @@ bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
 /// merge in N^3
 void data_dpt::dp_merge()
 {
-  if(size()<2)
+  if(data.size()<2)
     return;
 
-  unsigned initial_size=size();
+  unsigned initial_size=data.size();
 
   unsigned from=0;
   unsigned to=0;
 
   /* look for similar elements */
-  for(const_iterator it1=begin(); it1!=end(); ++it1)
+  for(auto it1=data.cbegin(); it1!=data.cend(); ++it1)
   {
-    const_iterator it2=it1;
+    auto it2=it1;
     ++it2;
     /* all ok -- ends */
-    if(it2==end())
+    if(it2==data.cend())
       return;
 
-    for(; it2!=end(); ++it2)
+    for(; it2!=data.cend(); ++it2)
     {
       if(it1 == it2)
       {
         from=it2->eq_class;
         to=it1->eq_class;
-        erase(it2);
+        data.erase(it2);
         break;
       }
     }
   }
 
   /* merge */
-  for(iterator it3=begin(); it3!=end(); ++it3)
+  for(auto it3=data.begin(); it3!=data.end(); ++it3)
     if(it3->eq_class==from)
       it3->eq_class=to;
 
   /* strictly monotonous => converges */
-  assert(initial_size>size());
+  assert(initial_size>data.size());
 
   /* repeat until classes are disjunct */
   dp_merge();
@@ -160,10 +160,10 @@ void data_dpt::dp_merge()
 void data_dpt::print(messaget &message)
 {
 #ifdef DEBUG
-  const_iterator it;
+  data_typet::const_iterator it;
   std::map<unsigned, std::set<source_locationt> > classed;
 
-  for(it=begin(); it!=end(); ++it)
+  for(it=data.cbegin(); it!=data.cend(); ++it)
   {
     if(classed.find(it->eq_class)==classed.end())
     {
diff --git a/src/goto-instrument/wmm/data_dp.h b/src/goto-instrument/wmm/data_dp.h
index abd7641fb9c..bdd3e1705c6 100644
--- a/src/goto-instrument/wmm/data_dp.h
+++ b/src/goto-instrument/wmm/data_dp.h
@@ -48,11 +48,13 @@ struct datat
   }
 };
 
-class data_dpt:public std::set<datat>
+class data_dpt final
 {
-public:
+  typedef std::set<datat> data_typet;
+  data_typet data;
   unsigned class_nb;
 
+public:
   /* add this dependency in the structure */
   void dp_analysis(const abstract_eventt &read, const abstract_eventt &write);
   void dp_analysis(

From d9c3fdbc61c1d6b6d3854e29fda7ee9af1d46ae0 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 12:40:50 +0100
Subject: [PATCH 03/14] Remove inheritance from list in event_graph.h

Whitespace fix
---
 src/goto-instrument/wmm/cycle_collection.cpp |  2 +-
 src/goto-instrument/wmm/event_graph.cpp      |  2 +-
 src/goto-instrument/wmm/event_graph.h        | 65 +++++++++++++++-----
 3 files changed, 53 insertions(+), 16 deletions(-)

diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp
index 64b619c4369..24bceab723c 100644
--- a/src/goto-instrument/wmm/cycle_collection.cpp
+++ b/src/goto-instrument/wmm/cycle_collection.cpp
@@ -25,7 +25,7 @@ void event_grapht::graph_explorert::filter_thin_air(
   {
     std::set<critical_cyclet>::const_iterator next=it;
     ++next;
-    critical_cyclet::const_iterator e_it=it->begin();
+    auto e_it=it->begin();
     /* is there an event in the cycle not in thin-air events? */
     for(; e_it!=it->end(); ++e_it)
       if(thin_air_events.find(*e_it)==thin_air_events.end())
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
index d5d9df2aff4..110a3618ea2 100644
--- a/src/goto-instrument/wmm/event_graph.cpp
+++ b/src/goto-instrument/wmm/event_graph.cpp
@@ -1427,7 +1427,7 @@ std::string event_grapht::critical_cyclet::print_name(
 
   if(first_done)
   {
-    critical_cyclet::size_type n_events=extra_fence_count;
+    auto n_events=extra_fence_count;
     for(std::string::const_iterator it=name.begin();
         it!=name.end();
         ++it)
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index e77a7e92d3a..7d69cbe8af6 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -35,9 +35,11 @@ class event_grapht
 {
 public:
   /* critical cycle */
-  class critical_cyclet:public std::list<event_idt>
+  class critical_cyclet final
   {
-  protected:
+    typedef std::list<event_idt> data_typet;
+    data_typet data;
+
     event_grapht &egraph;
 
     bool is_not_uniproc() const;
@@ -50,16 +52,48 @@ class event_grapht
     std::string print_name(const critical_cyclet &redyced,
       memory_modelt model) const;
 
-    bool check_AC(const_iterator s_it, const abstract_eventt &first,
+    bool check_AC(
+      data_typet::const_iterator s_it,
+      const abstract_eventt &first,
       const abstract_eventt &second) const;
-    bool check_BC(const_iterator it, const abstract_eventt &first,
+    bool check_BC(
+      data_typet::const_iterator it,
+      const abstract_eventt &first,
       const abstract_eventt &second) const;
 
   public:
     unsigned id;
-
     bool has_user_defined_fence;
 
+    // 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;
+
+    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(); }
+
+    template <typename T>
+    void push_front(T &&t) { data.push_front(std::forward<T>(t)); }
+
+    template <typename T>
+    void push_back(T &&t) { data.push_back(std::forward<T>(t)); }
+
+    value_type &front() { return data.front(); }
+    const value_type &front() const { return data.front(); }
+
+    value_type &back() { return data.back(); }
+    const value_type &back() const { return data.back(); }
+
+    size_t size() const { return data.size(); }
+
     critical_cyclet(event_grapht &_egraph, unsigned _id)
       :egraph(_egraph), id(_id), has_user_defined_fence(false)
     {
@@ -67,23 +101,26 @@ class event_grapht
 
     void operator()(const critical_cyclet &cyc)
     {
-      clear();
-      for(const_iterator it=cyc.begin(); it!=cyc.end(); it++)
-        push_back(*it);
+      data.clear();
+      for(
+        auto it=cyc.data.cbegin();
+        it!=cyc.data.cend();
+        ++it)
+        data.push_back(*it);
       has_user_defined_fence=cyc.has_user_defined_fence;
     }
 
     bool is_cycle()
     {
       /* size check */
-      if(size()<4)
+      if(data.size()<4)
         return false;
 
       /* po order check */
-      const_iterator it=begin();
-      const_iterator n_it=it;
+      auto it=data.cbegin();
+      auto n_it=it;
       ++n_it;
-      for(; it!=end() && n_it!=end(); ++it, ++n_it)
+      for(; it!=data.cend() && n_it!=data.cend(); ++it, ++n_it)
       {
         if(egraph[*it].thread==egraph[*n_it].thread
           && !egraph.are_po_ordered(*it, *n_it))
@@ -177,7 +214,7 @@ class event_grapht
       {
         critical_cyclet reduced(egraph, id);
         this->hide_internals(reduced);
-        assert(!reduced.empty());
+        assert(!reduced.data.empty());
         return print_name(reduced, model);
       }
       else
@@ -196,7 +233,7 @@ class event_grapht
 
     bool operator<(const critical_cyclet &other) const
     {
-      return ( ((std::list<event_idt>) *this) < (std::list<event_idt>)other);
+      return data<other.data;
     }
   };
 

From 4235157161f37c73607e816ad80c78668aff1b93 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 13:04:51 +0100
Subject: [PATCH 04/14] Remove inheritance from map in cfg.h

---
 src/goto-programs/cfg.h | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index 2e1bd83598b..1bc6289c798 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -64,11 +64,30 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
 public:
   typedef std::size_t entryt;
 
-  struct entry_mapt:
-    public std::map<goto_programt::const_targett, entryt>
+  class entry_mapt final
   {
+    typedef std::map<goto_programt::const_targett, entryt> data_typet;
+    data_typet data;
+
+  public:
     grapht< cfg_base_nodet<T, I> > &container;
 
+    // NOLINTNEXTLINE(readability/identifiers)
+    typedef data_typet::iterator iterator;
+    // NOLINTNEXTLINE(readability/identifiers)
+    typedef data_typet::const_iterator const_iterator;
+
+    template <typename U>
+    const_iterator find(U &&u) const { return data.find(std::forward<U>(u)); }
+
+    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(); }
+
     explicit entry_mapt(grapht< cfg_base_nodet<T, I> > &_container):
       container(_container)
     {
@@ -76,7 +95,7 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
 
     entryt &operator[](const goto_programt::const_targett &t)
     {
-      std::pair<iterator, bool> e=insert(std::make_pair(t, 0));
+      auto e=data.insert(std::make_pair(t, 0));
 
       if(e.second)
         e.first->second=container.add_node();

From 280c4fc85b0d064c925d6749fa21170c5e50ea62 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 13:06:56 +0100
Subject: [PATCH 05/14] Remove inheritance from list in format_strings.h

---
 src/goto-programs/format_strings.h | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/goto-programs/format_strings.h b/src/goto-programs/format_strings.h
index 8c233324ecf..502acfb311a 100644
--- a/src/goto-programs/format_strings.h
+++ b/src/goto-programs/format_strings.h
@@ -84,9 +84,7 @@ class format_tokent
   irep_idt value; // for text and pattern matching
 };
 
-class format_token_listt:public std::list<format_tokent>
-{
-};
+typedef std::list<format_tokent> format_token_listt;
 
 format_token_listt parse_format_string(const std::string &);
 

From 93ca04bf107c5b8f1dc013c42e6d1464cefe21cd Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 13:11:28 +0100
Subject: [PATCH 06/14] Remove inheritance from vector in ilp.h

---
 src/musketeer/ilp.h | 21 +++++----------------
 1 file changed, 5 insertions(+), 16 deletions(-)

diff --git a/src/musketeer/ilp.h b/src/musketeer/ilp.h
index b8cbe4e9202..c7ce87537a5 100644
--- a/src/musketeer/ilp.h
+++ b/src/musketeer/ilp.h
@@ -22,26 +22,15 @@ Author: Vincent Nimal
 class ilpt
 {
 protected:
-  template <class T>
-  class my_vectort: public std::vector<T>
-  {
-  public:
-    T *to_array()
-    {
-      /* NOTE: not valid if T==bool */
-      return &(*this)[0];
-    }
-  };
-
   glp_iocp parm;
   unsigned matrix_size;
 
 public:
   glp_prob *lp;
 
-  my_vectort<int> imat;
-  my_vectort<int> jmat;
-  my_vectort<double> vmat;
+  std::vector<int> imat;
+  std::vector<int> jmat;
+  std::vector<double> vmat;
 
   ilpt()
   {
@@ -69,8 +58,8 @@ class ilpt
 
   void solve()
   {
-    glp_load_matrix(lp, matrix_size, imat.to_array(),
-      jmat.to_array(), vmat.to_array());
+    glp_load_matrix(lp, matrix_size, imat.data(),
+      jmat.data(), vmat.data());
     glp_intopt(lp, &parm);
   }
 };

From e5baaa80e04b7ad874ed7a1215736a8b6475da66 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 13:28:04 +0100
Subject: [PATCH 07/14] Remove inheritance from set in
 propagate_const_function_pointers.cpp

---
 .../propagate_const_function_pointers.cpp     | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/musketeer/propagate_const_function_pointers.cpp b/src/musketeer/propagate_const_function_pointers.cpp
index eca3648c285..e58efe92429 100644
--- a/src/musketeer/propagate_const_function_pointers.cpp
+++ b/src/musketeer/propagate_const_function_pointers.cpp
@@ -114,12 +114,25 @@ class const_function_pointer_propagationt
     unsigned stack_scope);
 
   /* to keep track of the constant function pointers passed as arguments */
-  class arg_stackt: public std::set<irep_idt>
+  class arg_stackt final
   {
-  protected:
+    typedef std::set<irep_idt> data_typet;
+    data_typet data;
     const_function_pointer_propagationt &cfpp;
 
   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;
+
+    std::pair<iterator, bool> insert(const value_type &t)
+    {
+      return data.insert(t);
+    }
+
     explicit arg_stackt(const_function_pointer_propagationt &_cfpp):
       cfpp(_cfpp)
     {}
@@ -415,7 +428,7 @@ void const_function_pointer_propagationt::arg_stackt::add_args(
 void const_function_pointer_propagationt::arg_stackt::remove_args()
 {
   /* remove the parameter names */
-  for(const_iterator arg_it=begin(); arg_it!=end(); ++arg_it)
+  for(const_iterator arg_it=data.begin(); arg_it!=data.end(); ++arg_it)
   {
     cfpp.remove(*arg_it);
     cfpp.message.debug() << "SET: remove " << *arg_it << messaget::eom;

From 3b5263ffefb4f69e66d9d0cad0bed13538899731 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 14:16:15 +0100
Subject: [PATCH 08/14] Remove inheritance from map in value_set.h

---
 src/pointer-analysis/value_set.cpp | 22 +++++++-------
 src/pointer-analysis/value_set.h   | 46 +++++++++++++++++++++++++-----
 2 files changed, 50 insertions(+), 18 deletions(-)

diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 28b5bf360a0..34bb8265df8 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
 
 #include "add_failed_symbols.h"
 
-const value_sett::object_map_dt value_sett::object_map_dt::blank;
+const value_sett::object_map_dt value_sett::object_map_dt::blank{};
 object_numberingt value_sett::object_numbering;
 
 bool value_sett::field_sensitive(
@@ -74,7 +74,7 @@ bool value_sett::insert(
   unsigned n,
   const objectt &object) const
 {
-  object_map_dt::const_iterator entry=dest.read().find(n);
+  auto entry=dest.read().find(n);
 
   if(entry==dest.read().end())
   {
@@ -184,9 +184,9 @@ void value_sett::output(
   }
 }
 
-exprt value_sett::to_expr(object_map_dt::const_iterator it) const
+exprt value_sett::to_expr(const object_map_dt::value_type &it) const
 {
-  const exprt &object=object_numbering[it->first];
+  const exprt &object=object_numbering[it.first];
 
   if(object.id()==ID_invalid ||
      object.id()==ID_unknown)
@@ -196,8 +196,8 @@ exprt value_sett::to_expr(object_map_dt::const_iterator it) const
 
   od.object()=object;
 
-  if(it->second.offset_is_set)
-    od.offset()=from_integer(it->second.offset, index_type());
+  if(it.second.offset_is_set)
+    od.offset()=from_integer(it.second.offset, index_type());
 
   od.type()=od.object().type();
 
@@ -251,7 +251,7 @@ bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const
       it!=src.read().end();
       it++)
   {
-    if(insert(dest, it))
+    if(insert(dest, *it))
       result=true;
   }
 
@@ -323,7 +323,7 @@ void value_sett::get_value_set(
       it=object_map.read().begin();
       it!=object_map.read().end();
       it++)
-    dest.push_back(to_expr(it));
+    dest.push_back(to_expr(*it));
 
   #if 0
   for(value_setst::valuest::const_iterator it=dest.begin();
@@ -918,7 +918,7 @@ void value_sett::get_reference_set(
       it=object_map.read().begin();
       it!=object_map.read().end();
       it++)
-    dest.push_back(to_expr(it));
+    dest.push_back(to_expr(*it));
 }
 
 void value_sett::get_reference_set_rec(
@@ -1267,7 +1267,7 @@ void value_sett::do_free(
           to_dynamic_object_expr(object);
 
         if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, o_it);
+          set(new_object_map, *o_it);
         else
         {
           // adjust
@@ -1279,7 +1279,7 @@ void value_sett::do_free(
         }
       }
       else
-        set(new_object_map, o_it);
+        set(new_object_map, *o_it);
     }
 
     if(changed)
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 66e4fa57ab0..b07869aed4a 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -58,25 +58,57 @@ class value_sett
     { return offset_is_set && offset.is_zero(); }
   };
 
-  class object_map_dt:public std::map<unsigned, objectt>
+  class object_map_dt
   {
+    typedef std::map<unsigned, objectt> data_typet;
+    data_typet data;
+
   public:
-    object_map_dt() {}
+    // 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;
+
+    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(); }
+
+    objectt &operator[](unsigned i) { return data[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)); }
+
     static const object_map_dt blank;
+
+    object_map_dt()=default;
+
+  protected:
+    ~object_map_dt()=default;
   };
 
-  exprt to_expr(object_map_dt::const_iterator it) const;
+  exprt to_expr(const object_map_dt::value_type &it) const;
 
   typedef reference_counting<object_map_dt> object_mapt;
 
-  void set(object_mapt &dest, object_map_dt::const_iterator it) const
+  void set(object_mapt &dest, const object_map_dt::value_type &it) const
   {
-    dest.write()[it->first]=it->second;
+    dest.write()[it.first]=it.second;
   }
 
-  bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
+  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
   {
-    return insert(dest, it->first, it->second);
+    return insert(dest, it.first, it.second);
   }
 
   bool insert(object_mapt &dest, const exprt &src) const

From b6ca04c9b0d74d3133e93c7953b614b191717d9d Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 14:25:53 +0100
Subject: [PATCH 09/14] Remove inheritance from map in value_set_fi.h

---
 src/pointer-analysis/value_set_fi.cpp | 33 ++++++++++----------
 src/pointer-analysis/value_set_fi.h   | 44 ++++++++++++++++++++++-----
 2 files changed, 54 insertions(+), 23 deletions(-)

diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index d08694b82da..968834fa9d7 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -25,7 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_util.h>
 #include <util/c_types.h>
 
-const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank;
+const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank{};
+
 object_numberingt value_set_fit::object_numbering;
 hash_numbering<irep_idt, irep_id_hash> value_set_fit::function_numbering;
 
@@ -206,11 +207,11 @@ void value_set_fit::flatten_rec(
         }
 
         forall_objects(oit, temp.read())
-          insert(dest, oit);
+          insert(dest, *oit);
       }
     }
     else
-      insert(dest, it);
+      insert(dest, *it);
   }
 
   if(generalize_index) // this means we had recursive symbols in there
@@ -222,9 +223,9 @@ void value_set_fit::flatten_rec(
   seen.erase(identifier + e.suffix);
 }
 
-exprt value_set_fit::to_expr(object_map_dt::const_iterator it) const
+exprt value_set_fit::to_expr(const object_map_dt::value_type &it) const
 {
-  const exprt &object=object_numbering[it->first];
+  const exprt &object=object_numbering[it.first];
 
   if(object.id()==ID_invalid ||
      object.id()==ID_unknown)
@@ -234,8 +235,8 @@ exprt value_set_fit::to_expr(object_map_dt::const_iterator it) const
 
   od.object()=object;
 
-  if(it->second.offset_is_set)
-    od.offset()=from_integer(it->second.offset, index_type());
+  if(it.second.offset_is_set)
+    od.offset()=from_integer(it.second.offset, index_type());
 
   od.type()=od.object().type();
 
@@ -287,7 +288,7 @@ bool value_set_fit::make_union(object_mapt &dest, const object_mapt &src) const
 
   forall_objects(it, src.read())
   {
-    if(insert(dest, it))
+    if(insert(dest, *it))
       result=true;
   }
 
@@ -340,7 +341,7 @@ void value_set_fit::get_value_set(
   }
 
   forall_objects(fit, flat_map.read())
-    value_set.push_back(to_expr(fit));
+    value_set.push_back(to_expr(*fit));
 
   #if 0
   // Sanity check!
@@ -744,11 +745,11 @@ void value_set_fit::get_reference_set(
         }
 
         forall_objects(it, omt.read())
-          dest.insert(to_expr(it));
+          dest.insert(to_expr(*it));
       }
     }
     else
-      dest.insert(to_expr(it));
+      dest.insert(to_expr(*it));
   }
 }
 
@@ -761,7 +762,7 @@ void value_set_fit::get_reference_set_sharing(
   get_reference_set_sharing(expr, object_map, ns);
 
   forall_objects(it, object_map.read())
-    dest.insert(to_expr(it));
+    dest.insert(to_expr(*it));
 }
 
 void value_set_fit::get_reference_set_sharing_rec(
@@ -833,13 +834,13 @@ void value_set_fit::get_reference_set_sharing_rec(
           }
 
           forall_objects(it2, t2.read())
-            insert(dest, it2);
+            insert(dest, *it2);
         }
         else
           insert(dest, exprt(ID_unknown, obj.type().subtype()));
       }
       else
-        insert(dest, it);
+        insert(dest, *it);
     }
 
     #if 0
@@ -1182,7 +1183,7 @@ void value_set_fit::do_free(
           to_dynamic_object_expr(object);
 
         if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, o_it);
+          set(new_object_map, *o_it);
         else
         {
           // adjust
@@ -1194,7 +1195,7 @@ void value_set_fit::do_free(
         }
       }
       else
-        set(new_object_map, o_it);
+        set(new_object_map, *o_it);
     }
 
     if(changed)
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index cc69a4f59a8..77d4c1f54ec 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -71,25 +71,55 @@ class value_set_fit
     { return offset_is_set && offset.is_zero(); }
   };
 
-  class object_map_dt:public std::map<unsigned, objectt>
+  class object_map_dt
   {
+    typedef std::map<unsigned, objectt> data_typet;
+    data_typet data;
+
   public:
-    object_map_dt() {}
+    // 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;
+
+    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(); }
+
+    objectt &operator[](unsigned i) { return data[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)); }
+
     static const object_map_dt blank;
+
+  protected:
+    ~object_map_dt()=default;
   };
 
-  exprt to_expr(object_map_dt::const_iterator it) const;
+  exprt to_expr(const object_map_dt::value_type &it) const;
 
   typedef reference_counting<object_map_dt> object_mapt;
 
-  void set(object_mapt &dest, object_map_dt::const_iterator it) const
+  void set(object_mapt &dest, const object_map_dt::value_type &it) const
   {
-    dest.write()[it->first]=it->second;
+    dest.write()[it.first]=it.second;
   }
 
-  bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
+  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
   {
-    return insert(dest, it->first, it->second);
+    return insert(dest, it.first, it.second);
   }
 
   bool insert(object_mapt &dest, const exprt &src) const

From e2a13beccfcbeb7b43a89f2bf28f719ef5381e2b Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 14:54:06 +0100
Subject: [PATCH 10/14] Remove inheritance from vector in expanding_vector.h

---
 src/analyses/local_bitvector_analysis.cpp | 36 +++++++++----------
 src/analyses/local_bitvector_analysis.h   | 17 +++------
 src/util/expanding_vector.h               | 43 ++++++++++++++---------
 3 files changed, 48 insertions(+), 48 deletions(-)

diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index f48b34a760d..341eab33d42 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -41,16 +41,16 @@ void local_bitvector_analysist::flagst::print(std::ostream &out) const
     out << "+integer_address";
 }
 
-bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
+bool local_bitvector_analysist::merge(points_tot &a, points_tot &b)
 {
   bool result=false;
 
   std::size_t max_index=
-    std::max(src.points_to.size(), points_to.size());
+    std::max(a.size(), b.size());
 
   for(std::size_t i=0; i<max_index; i++)
   {
-    if(points_to[i].merge(src.points_to[i]))
+    if(a[i].merge(b[i]))
       result=true;
   }
 
@@ -72,8 +72,8 @@ bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
 void local_bitvector_analysist::assign_lhs(
   const exprt &lhs,
   const exprt &rhs,
-  const loc_infot &loc_info_src,
-  loc_infot &loc_info_dest)
+  points_tot &loc_info_src,
+  points_tot &loc_info_dest)
 {
   if(lhs.id()==ID_symbol)
   {
@@ -83,7 +83,7 @@ void local_bitvector_analysist::assign_lhs(
     {
       unsigned dest_pointer=pointers.number(identifier);
       flagst rhs_flags=get_rec(rhs, loc_info_src);
-      loc_info_dest.points_to[dest_pointer]=rhs_flags;
+      loc_info_dest[dest_pointer]=rhs_flags;
     }
   }
   else if(lhs.id()==ID_dereference)
@@ -117,14 +117,12 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get(
 
   assert(loc_it!=cfg.loc_map.end());
 
-  const loc_infot &loc_info_src=loc_infos[loc_it->second];
-
-  return get_rec(rhs, loc_info_src);
+  return get_rec(rhs, loc_infos[loc_it->second]);
 }
 
 local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
   const exprt &rhs,
-  const loc_infot &loc_info_src)
+  points_tot &loc_info_src)
 {
   if(rhs.id()==ID_constant)
   {
@@ -139,7 +137,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
     if(is_tracked(identifier))
     {
       unsigned src_pointer=pointers.number(identifier);
-      return loc_info_src.points_to[src_pointer];
+      return loc_info_src[src_pointer];
     }
     else
       return flagst::mk_unknown();
@@ -258,7 +256,7 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
   // in the entry location.
   for(const auto &local : locals.locals_map)
     if(is_tracked(local.first))
-      loc_infos[0].points_to[pointers.number(local.first)]=flagst::mk_unknown();
+      loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown();
 
   while(!work_queue.empty())
   {
@@ -267,8 +265,8 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
     const goto_programt::instructiont &instruction=*node.t;
     work_queue.pop();
 
-    const loc_infot &loc_info_src=loc_infos[loc_nr];
-    loc_infot loc_info_dest=loc_infos[loc_nr];
+    auto &loc_info_src=loc_infos[loc_nr];
+    auto loc_info_dest=loc_infos[loc_nr];
 
     switch(instruction.type)
     {
@@ -320,7 +318,7 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
     for(const auto &succ : node.successors)
     {
       assert(succ<loc_infos.size());
-      if(loc_infos[succ].merge(loc_info_dest))
+      if(merge(loc_infos[succ], (loc_info_dest)))
         work_queue.push(succ);
     }
   }
@@ -337,14 +335,14 @@ void local_bitvector_analysist::output(
   {
     out << "**** " << i_it->source_location << "\n";
 
-    const loc_infot &loc_info=loc_infos[l];
+    const auto &loc_info=loc_infos[l];
 
     for(points_tot::const_iterator
-        p_it=loc_info.points_to.begin();
-        p_it!=loc_info.points_to.end();
+        p_it=loc_info.begin();
+        p_it!=loc_info.end();
         p_it++)
     {
-      out << "  " << pointers[p_it-loc_info.points_to.begin()]
+      out << "  " << pointers[p_it-loc_info.begin()]
           << ": "
           << *p_it
           << "\n";
diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h
index a88b38fb1c6..4a750d8cf32 100644
--- a/src/analyses/local_bitvector_analysis.h
+++ b/src/analyses/local_bitvector_analysis.h
@@ -186,27 +186,20 @@ class local_bitvector_analysist
   // This is a vector, so it's fast.
   typedef expanding_vectort<flagst> points_tot;
 
-  // the information tracked per program location
-  class loc_infot
-  {
-  public:
-    points_tot points_to;
-
-    bool merge(const loc_infot &src);
-  };
+  static bool merge(points_tot &a, points_tot &b);
 
-  typedef std::vector<loc_infot> loc_infost;
+  typedef std::vector<points_tot> loc_infost;
   loc_infost loc_infos;
 
   void assign_lhs(
     const exprt &lhs,
     const exprt &rhs,
-    const loc_infot &loc_info_src,
-    loc_infot &loc_info_dest);
+    points_tot &loc_info_src,
+    points_tot &loc_info_dest);
 
   flagst get_rec(
     const exprt &rhs,
-    const loc_infot &loc_info_src);
+    points_tot &loc_info_src);
 
   bool is_tracked(const irep_idt &identifier);
 };
diff --git a/src/util/expanding_vector.h b/src/util/expanding_vector.h
index f8b0421db72..8c2af9cdb3f 100644
--- a/src/util/expanding_vector.h
+++ b/src/util/expanding_vector.h
@@ -13,31 +13,40 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <vector>
 
 template<typename T>
-class expanding_vectort:public std::vector<T>
+class expanding_vectort
 {
+  typedef std::vector<T> data_typet;
+  data_typet data;
+
 public:
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::size_type size_type;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::const_iterator const_iterator;
+
   T &operator[] (typename std::vector<T>::size_type n)
   {
-    check_index(n);
-    return subt::operator[](n);
+    if(n>=data.size())
+      data.resize(n+1);
+    return data[n];
   }
 
-  const T &operator[] (typename std::vector<T>::size_type n) const
-  {
-    // hack-ish const cast
-    const_cast<expanding_vectort*>(this)->check_index(n);
-    return subt::operator[](n);
-  }
+  void clear() { data.clear(); }
 
-protected:
-  typedef std::vector<T> subt;
+  iterator begin() { return data.begin(); }
+  const_iterator begin() const { return data.begin(); }
+  const_iterator cbegin() const { return data.cbegin(); }
 
-  // make the vector large enough to contain 'n'
-  void check_index(typename std::vector<T>::size_type n)
-  {
-    if(n>=subt::size())
-      subt::resize(n+1);
-  }
+  iterator end() { return data.end(); }
+  const_iterator end() const { return data.end(); }
+  const_iterator cend() const { return data.cend(); }
+
+  size_type size() const { return data.size(); }
+
+  void push_back(const T &t) { data.push_back(t); }
+  void push_back(T &&t) { data.push_back(std::move(t)); }
 };
 
 #endif // CPROVER_UTIL_EXPANDING_VECTOR_H

From 3fa38437180783082d99c7d65440f80bbc66c5a7 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 13 May 2017 18:31:25 +0100
Subject: [PATCH 11/14] Remove inheritance from std containers in numbering.h

Squash
---
 src/util/numbering.h  | 73 ++++++++++++++++++++++++++++++++++---------
 src/util/union_find.h | 66 ++++++++++++++++++++++++++------------
 2 files changed, 105 insertions(+), 34 deletions(-)

diff --git a/src/util/numbering.h b/src/util/numbering.h
index 359f3c48ed2..55a6231f16d 100644
--- a/src/util/numbering.h
+++ b/src/util/numbering.h
@@ -18,12 +18,26 @@ Author: Daniel Kroening, kroening@kroening.com
 
 template <typename T>
 // NOLINTNEXTLINE(readability/identifiers)
-class numbering:public std::vector<T>
+class numbering final
 {
 public:
   // NOLINTNEXTLINE(readability/identifiers)
   typedef std::size_t number_type;
 
+private:
+  typedef std::vector<T> data_typet;
+  data_typet data;
+  typedef std::map<T, number_type> numberst;
+  numberst numbers;
+
+public:
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::size_type size_type;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::const_iterator const_iterator;
+
   number_type number(const T &a)
   {
     std::pair<typename numberst::const_iterator, bool> result=
@@ -33,8 +47,8 @@ class numbering:public std::vector<T>
 
     if(result.second) // inserted?
     {
-      this->push_back(a);
-      assert(this->size()==numbers.size());
+      data.push_back(a);
+      assert(data.size()==numbers.size());
     }
 
     return (result.first)->second;
@@ -58,25 +72,46 @@ class numbering:public std::vector<T>
 
   void clear()
   {
-    subt::clear();
+    data.clear();
     numbers.clear();
   }
 
-protected:
-  typedef std::vector<T> subt;
+  size_t size() const { return data.size(); }
 
-  typedef std::map<T, number_type> numberst;
-  numberst numbers;
+  T &operator[](size_type t) { return data[t]; }
+  const T &operator[](size_type t) const { return data[t]; }
+
+  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(); }
 };
 
 template <typename T, class hash_fkt>
 // NOLINTNEXTLINE(readability/identifiers)
-class hash_numbering:public std::vector<T>
+class hash_numbering final
 {
 public:
   // NOLINTNEXTLINE(readability/identifiers)
   typedef unsigned int number_type;
 
+private:
+  typedef std::vector<T> data_typet;
+  data_typet data;
+  typedef std::unordered_map<T, number_type, hash_fkt> numberst;
+  numberst numbers;
+
+public:
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::size_type size_type;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename data_typet::const_iterator const_iterator;
+
   number_type number(const T &a)
   {
     std::pair<typename numberst::const_iterator, bool> result=
@@ -106,15 +141,25 @@ class hash_numbering:public std::vector<T>
 
   void clear()
   {
-    subt::clear();
+    data.clear();
     numbers.clear();
   }
 
-protected:
-  typedef std::vector<T> subt;
+  template <typename U>
+  void push_back(U &&u) { data.push_back(std::forward<U>(u)); }
 
-  typedef std::unordered_map<T, number_type, hash_fkt> numberst;
-  numberst numbers;
+  T &operator[](size_type t) { return data[t]; }
+  const T &operator[](size_type t) const { return data[t]; }
+
+  size_type size() const { return data.size(); }
+
+  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(); }
 };
 
 #endif // CPROVER_UTIL_NUMBERING_H
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 4908bf65a49..7369343cff5 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -130,11 +130,21 @@ class unsigned_union_find
 
 template <typename T>
 // NOLINTNEXTLINE(readability/identifiers)
-class union_find:public numbering<T>
+class union_find final
 {
+  typedef numbering<T> numbering_typet;
+  numbering_typet numbers;
+
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename numbering_typet::number_type number_type;
+
 public:
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef typename numbering<T>::size_type size_type;
+  typedef typename numbering_typet::size_type size_type;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename numbering_typet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)
+  typedef typename numbering_typet::const_iterator const_iterator;
 
   // true == already in same set
   bool make_union(const T &a, const T &b)
@@ -149,7 +159,7 @@ class union_find:public numbering<T>
   bool make_union(typename numbering<T>::const_iterator it_a,
                   typename numbering<T>::const_iterator it_b)
   {
-    size_type na=it_a-numbering<T>::begin(), nb=it_b-numbering<T>::begin();
+    size_type na=it_a-numbers.begin(), nb=it_b-numbers.begin();
     bool is_union=find_number(na)==find_number(nb);
     uuf.make_union(na, nb);
     return is_union;
@@ -158,10 +168,9 @@ class union_find:public numbering<T>
   // are 'a' and 'b' in the same set?
   bool same_set(const T &a, const T &b) const
   {
-    typedef typename subt::number_type subt_number_typet;
-    subt_number_typet na=subt_number_typet(), nb=subt_number_typet();
-    bool have_na=!subt::get_number(a, na),
-         have_nb=!subt::get_number(b, nb);
+    number_type na, nb;
+    bool have_na=!numbers.get_number(a, na),
+         have_nb=!numbers.get_number(b, nb);
 
     if(have_na && have_nb)
       return uuf.same_set(na, nb);
@@ -175,22 +184,22 @@ class union_find:public numbering<T>
   bool same_set(typename numbering<T>::const_iterator it_a,
                 typename numbering<T>::const_iterator it_b) const
   {
-    return uuf.same_set(it_a-numbering<T>::begin(), it_b-numbering<T>::begin());
+    return uuf.same_set(it_a-numbers.begin(), it_b-numbers.begin());
   }
 
   const T &find(typename numbering<T>::const_iterator it) const
   {
-    return numbering<T>::operator[](find_number(it-numbering<T>::begin()));
+    return numbers[find_number(it-numbers.begin())];
   }
 
   const T &find(const T &a)
   {
-    return numbering<T>::operator[](find_number(number(a)));
+    return numbers[find_number(number(a))];
   }
 
   size_type find_number(typename numbering<T>::const_iterator it) const
   {
-    return find_number(it-numbering<T>::begin());
+    return find_number(it-numbers.begin());
   }
 
   size_type find_number(size_type a) const
@@ -210,9 +219,8 @@ class union_find:public numbering<T>
 
   bool is_root(const T &a) const
   {
-    typename subt::number_type na;
-
-    if(subt::get_number(a, na))
+    number_type na;
+    if(numbers.get_number(a, na))
       return true; // not found, it's a root
     else
       return uuf.is_root(na);
@@ -220,30 +228,30 @@ class union_find:public numbering<T>
 
   bool is_root(typename numbering<T>::const_iterator it) const
   {
-    return uuf.is_root(it-numbering<T>::begin());
+    return uuf.is_root(it-numbers.begin());
   }
 
   size_type number(const T &a)
   {
-    size_type n=subt::number(a);
+    size_type n=numbers.number(a);
 
     if(n>=uuf.size())
-      uuf.resize(this->size());
+      uuf.resize(numbers.size());
 
-    assert(uuf.size()==this->size());
+    assert(uuf.size()==numbers.size());
 
     return n;
   }
 
   void clear()
   {
-    subt::clear();
+    numbers.clear();
     uuf.clear();
   }
 
   void isolate(typename numbering<T>::const_iterator it)
   {
-    uuf.isolate(it-numbering<T>::begin());
+    uuf.isolate(it-numbers.begin());
   }
 
   void isolate(const T &a)
@@ -251,6 +259,24 @@ class union_find:public numbering<T>
     uuf.isolate(number(a));
   }
 
+  bool get_number(const T &a, number_type &n) const
+  {
+    return numbers.get_number(a, n);
+  }
+
+  size_t size() const { return numbers.size(); }
+
+  T &operator[](size_type t) { return numbers[t]; }
+  const T &operator[](size_type t) const { return numbers[t]; }
+
+  iterator begin() { return numbers.begin(); }
+  const_iterator begin() const { return numbers.begin(); }
+  const_iterator cbegin() const { return numbers.cbegin(); }
+
+  iterator end() { return numbers.end(); }
+  const_iterator end() const { return numbers.end(); }
+  const_iterator cend() const { return numbers.cend(); }
+
 protected:
   unsigned_union_find uuf;
   typedef numbering<T> subt;

From 96062375fe42acfac2b0748ac26bcf93d0ba55f5 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Wed, 21 Jun 2017 10:19:40 +0100
Subject: [PATCH 12/14] Fix formatting in event graph

---
 src/goto-instrument/wmm/event_graph.h | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 7d69cbe8af6..076f8f679bf 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -102,10 +102,9 @@ class event_grapht
     void operator()(const critical_cyclet &cyc)
     {
       data.clear();
-      for(
-        auto it=cyc.data.cbegin();
-        it!=cyc.data.cend();
-        ++it)
+      for(auto it=cyc.data.cbegin();
+          it!=cyc.data.cend();
+          ++it)
         data.push_back(*it);
       has_user_defined_fence=cyc.has_user_defined_fence;
     }

From 39bee7772a3cf77646a541c0b3f1bf1d3a7b6620 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Wed, 21 Jun 2017 10:43:22 +0100
Subject: [PATCH 13/14] Add missing `empty`

---
 src/pointer-analysis/value_set.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index b07869aed4a..f30386e8eb5 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -80,6 +80,7 @@ class value_sett
     const_iterator cend() const { return data.cend(); }
 
     size_t size() const { return data.size(); }
+    bool empty() const { return data.empty(); }
 
     objectt &operator[](unsigned i) { return data[i]; }
 

From b00c377c050a21b1856bdc095b2456710f455ab5 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Wed, 21 Jun 2017 10:43:47 +0100
Subject: [PATCH 14/14] Fix invariant warnings

---
 src/goto-instrument/wmm/data_dp.cpp   | 3 ++-
 src/goto-instrument/wmm/event_graph.h | 3 ++-
 src/util/numbering.h                  | 3 ++-
 src/util/union_find.h                 | 2 +-
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/goto-instrument/wmm/data_dp.cpp b/src/goto-instrument/wmm/data_dp.cpp
index c9baff90f95..d88f20859eb 100644
--- a/src/goto-instrument/wmm/data_dp.cpp
+++ b/src/goto-instrument/wmm/data_dp.cpp
@@ -13,6 +13,7 @@ Date: 2012
 
 #include "data_dp.h"
 
+#include <util/invariant.h>
 #include <util/message.h>
 
 #include "abstract_event.h"
@@ -151,7 +152,7 @@ void data_dpt::dp_merge()
       it3->eq_class=to;
 
   /* strictly monotonous => converges */
-  assert(initial_size>data.size());
+  INVARIANT(initial_size>data.size(), "strictly monotonous => converges");
 
   /* repeat until classes are disjunct */
   dp_merge();
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 076f8f679bf..69eb502760d 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -20,6 +20,7 @@ Date: 2012
 #include <iosfwd>
 
 #include <util/graph.h>
+#include <util/invariant.h>
 
 #include "abstract_event.h"
 #include "data_dp.h"
@@ -213,7 +214,7 @@ class event_grapht
       {
         critical_cyclet reduced(egraph, id);
         this->hide_internals(reduced);
-        assert(!reduced.data.empty());
+        INVARIANT(!reduced.data.empty(), "reduced must not be empty");
         return print_name(reduced, model);
       }
       else
diff --git a/src/util/numbering.h b/src/util/numbering.h
index 55a6231f16d..4e0113a117a 100644
--- a/src/util/numbering.h
+++ b/src/util/numbering.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_map>
 #include <vector>
 
+#include <util/invariant.h>
 
 template <typename T>
 // NOLINTNEXTLINE(readability/identifiers)
@@ -48,7 +49,7 @@ class numbering final
     if(result.second) // inserted?
     {
       data.push_back(a);
-      assert(data.size()==numbers.size());
+      INVARIANT(data.size()==numbers.size(), "vector sizes must match");
     }
 
     return (result.first)->second;
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 7369343cff5..42dd4738735 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -238,7 +238,7 @@ class union_find final
     if(n>=uuf.size())
       uuf.resize(numbers.size());
 
-    assert(uuf.size()==numbers.size());
+    INVARIANT(uuf.size()==numbers.size(), "container sizes must match");
 
     return n;
   }