Disallow context-dependent copy/assignment.

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 3a7f56e174fc9533b2e9dfdcfc3d6e04409bbe0b..7fb36bb3ad7dc831164787999a23e3654d1bfba5 100644 (file)
--- 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 881c3f62905de6ddb61545302db3c1b2a4da031a..18a39754ebae2def1c65ae7be22c23e2bb5c35f9 100644 (file)
--- 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 fa86235d48233b07d65f82321d550b04e71c314d..f834e6b5fe0827764fd1c772c314454872cd7cab 100644 (file)
--- 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 c57a315f57f07a89ac3912facdadc577d68c9306..51f1dbfa715e667f687db301111e9c2060dcd69f 100644 (file)
--- 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 de83c4aa55ca015436652d48261c567fa69a9793..496af78153f3516f61d77cd4ee60bd42a89ffbc2 100644 (file)
--- 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 52e1d52bbca00d5846eacfa449b962c6c109a9ab..64e916680bd7be6099a26316866ce3260a6858a6 100644 (file)
--- 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 2b907ca2a03facbe283c1c8f3a84fe7df3fa2795..0285d47a84b89ade66def12b7255e67eab782993 100644 (file)
--- 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 */