diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-16 16:43:56 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:38 -0400 |
commit | 00ae9a7eba6648f957011cc250ba8707cce029c3 (patch) | |
tree | b127eb494d7cf70d2769b8f94781f8f464805561 | |
parent | bb35ed4f871e4cb5d33c1030fc5547bb92ec334b (diff) |
Disallow context-dependent copy/assignment.
-rw-r--r-- | src/context/cdhashmap.h | 5 | ||||
-rw-r--r-- | src/context/cdhashset.h | 6 | ||||
-rw-r--r-- | src/context/cdinsert_hashmap.h | 5 | ||||
-rw-r--r-- | src/context/cdlist.h | 3 | ||||
-rw-r--r-- | src/context/cdo.h | 2 | ||||
-rw-r--r-- | src/context/cdvector.h | 4 | ||||
-rw-r--r-- | 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 */ |