diff options
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/cdlist_forward.h | 2 | ||||
-rw-r--r-- | src/context/cdmap_forward.h | 2 | ||||
-rw-r--r-- | src/context/cdset_forward.h | 2 | ||||
-rw-r--r-- | src/context/context.h | 18 |
4 files changed, 12 insertions, 12 deletions
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h index 82bc9cc15..a1e50c7c8 100644 --- a/src/context/cdlist_forward.h +++ b/src/context/cdlist_forward.h @@ -37,7 +37,7 @@ #include <memory> namespace __gnu_cxx { - template <class Key> class hash; + template <class Key> struct hash; }/* __gnu_cxx namespace */ namespace CVC4 { diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h index 1024f0b54..214d9e700 100644 --- a/src/context/cdmap_forward.h +++ b/src/context/cdmap_forward.h @@ -29,7 +29,7 @@ #define __CVC4__CONTEXT__CDMAP_FORWARD_H namespace __gnu_cxx { - template <class Key> class hash; + template <class Key> struct hash; }/* __gnu_cxx namespace */ namespace CVC4 { diff --git a/src/context/cdset_forward.h b/src/context/cdset_forward.h index 135db8751..af3c6f85c 100644 --- a/src/context/cdset_forward.h +++ b/src/context/cdset_forward.h @@ -29,7 +29,7 @@ #define __CVC4__CONTEXT__CDSET_FORWARD_H namespace __gnu_cxx { - template <class Key> class hash; + template <class Key> struct hash; }/* __gnu_cxx namespace */ namespace CVC4 { diff --git a/src/context/context.h b/src/context/context.h index 053d5cb1a..aabe4e7c2 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -497,6 +497,15 @@ protected: public: /** + * Disable delete: objects allocated with new(ContextMemorymanager) should + * never be deleted. Objects allocated with new(bool) should be deleted by + * calling deleteSelf(). + */ + static void operator delete(void* pMem) { + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + } + + /** * operator new using ContextMemoryManager (common case used by * subclasses during save()). No delete is required for memory * allocated this way, since it is automatically released when the @@ -573,15 +582,6 @@ public: ::operator delete(this); } - /** - * Disable delete: objects allocated with new(ContextMemorymanager) should - * never be deleted. Objects allocated with new(bool) should be deleted by - * calling deleteSelf(). - */ - static void operator delete(void* pMem) { - AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); - } - };/* class ContextObj */ /** |