From 4d5f9f67adf51271ae92a10743b7410d960ff759 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 16 Jun 2014 16:43:56 -0400
Subject: [PATCH] Disallow context-dependent copy/assignment.

---
 src/context/cdhashmap.h        | 5 +++++
 src/context/cdhashset.h        | 6 +++++-
 src/context/cdinsert_hashmap.h | 5 +++--
 src/context/cdlist.h           | 3 ++-
 src/context/cdo.h              | 2 +-
 src/context/cdvector.h         | 4 ++++
 src/context/context.h          | 8 ++++----
 7 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 3a7f56e17..7fb36bb3a 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -174,6 +174,7 @@ class CDOhash_map : public ContextObj {
     d_prev(NULL),
     d_next(NULL) {
   }
+  CDOhash_map& operator=(const CDOhash_map&) CVC4_UNDEFINED;
 
 public:
 
@@ -305,6 +306,10 @@ class CDHashMap : public ContextObj {
     d_trash.clear();
   }
 
+  // no copy or assignment
+  CDHashMap(const CDHashMap&) CVC4_UNDEFINED;
+  CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED;
+
 public:
 
   CDHashMap(Context* context) :
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index 881c3f629..18a39754e 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -30,6 +30,10 @@ template <class V, class HashFcn>
 class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
   typedef CDInsertHashMap<V, bool, HashFcn> super;
 
+  // no copy or assignment
+  CDHashSet(const CDHashSet&) CVC4_UNDEFINED;
+  CDHashSet& operator=(const CDHashSet&) CVC4_UNDEFINED;
+
 public:
 
   // ensure these are publicly accessible
@@ -148,7 +152,7 @@ public:
     return super::insertAtContextLevelZero(v, true);
   }
 
-};/* class CDSet */
+};/* class CDHashSet */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index fa86235d4..f834e6b5f 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -179,7 +179,7 @@ public:
   }
 };/* class TrailHashMap<> */
 
-template <class Key, class Data, class HashFcn >
+template <class Key, class Data, class HashFcn>
 class CDInsertHashMap : public ContextObj {
 private:
   typedef InsertHashMap<Key, Data, HashFcn> IHM;
@@ -201,7 +201,7 @@ private:
    * not copied: only the base class information and
    * d_size and d_pushFronts are needed in restore.
    */
-  CDInsertHashMap(const CDInsertHashMap<Key, Data, HashFcn>& l) :
+  CDInsertHashMap(const CDInsertHashMap& l) :
     ContextObj(l),
     d_insertMap(NULL),
     d_size(l.d_size),
@@ -211,6 +211,7 @@ private:
                     << " from " << &l
                     << " size " << d_size << std::endl;
   }
+  CDInsertHashMap& operator=(const CDInsertHashMap&) CVC4_UNDEFINED;
 
   /**
    * Implementation of mandatory ContextObj method save: simply copies
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index c57a315f5..51f1dbfa7 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -103,7 +103,7 @@ protected:
    * d_sizeAlloc are not copied: only the base class information and
    * d_size are needed in restore.
    */
-  CDList(const CDList<T, CleanUp, Allocator>& l) :
+  CDList(const CDList& l) :
     ContextObj(l),
     d_list(NULL),
     d_size(l.d_size),
@@ -115,6 +115,7 @@ protected:
                     << " from " << &l
                     << " size " << d_size << std::endl;
   }
+  CDList& operator=(const CDList& l) CVC4_UNDEFINED;
 
 private:
   /**
diff --git a/src/context/cdo.h b/src/context/cdo.h
index de83c4aa5..496af7815 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -49,7 +49,7 @@ protected:
   /**
    * operator= for CDO is private to ensure CDO object is not copied.
    */
-  CDO<T>& operator=(const CDO<T>& cdo) CVC4_UNUSED;
+  CDO<T>& operator=(const CDO<T>& cdo) CVC4_UNDEFINED;
 
   /**
    * Implementation of mandatory ContextObj method save: simply copies the
diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index 52e1d52bb..64e916680 100644
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -86,6 +86,10 @@ private:
 
   Context* d_context;
 
+  // no copy or assignment
+  CDVector(const CDVector&) CVC4_UNDEFINED;
+  CDVector& operator=(const CDVector&) CVC4_UNDEFINED;
+
 public:
   CDVector(Context* c) :
     d_current(),
diff --git a/src/context/context.h b/src/context/context.h
index 2b907ca2a..0285d47a8 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -94,8 +94,8 @@ class Context {
   operator<<(std::ostream&, const Context&) throw(AssertionException);
 
   // disable copy, assignment
-  Context(const Context&) CVC4_UNUSED;
-  Context& operator=(const Context&) CVC4_UNUSED;
+  Context(const Context&) CVC4_UNDEFINED;
+  Context& operator=(const Context&) CVC4_UNDEFINED;
 
 public:
 
@@ -208,8 +208,8 @@ public:
 class UserContext : public Context {
 private:
   // disable copy, assignment
-  UserContext(const UserContext&) CVC4_UNUSED;
-  UserContext& operator=(const UserContext&) CVC4_UNUSED;
+  UserContext(const UserContext&) CVC4_UNDEFINED;
+  UserContext& operator=(const UserContext&) CVC4_UNDEFINED;
 public:
   UserContext() {}
 };/* class UserContext */
-- 
2.30.2