diff options
| -rw-r--r-- | configure.ac | 18 | ||||
| -rw-r--r-- | src/context/context_mm.cpp | 4 | ||||
| -rw-r--r-- | src/context/context_mm.h | 21 |
3 files changed, 28 insertions, 15 deletions
diff --git a/configure.ac b/configure.ac index 319b8d79f..ef12e4825 100644 --- a/configure.ac +++ b/configure.ac @@ -674,20 +674,20 @@ if test "$enable_valgrind" != no; then ]) fi -AC_MSG_CHECKING([whether to use the context memory manager]) +AC_MSG_CHECKING([whether to use the debug context memory manager]) -AC_ARG_ENABLE([context-memory-manager], - [AS_HELP_STRING([--disable-context-memory-manager], - [do not use the context memory manager])]) +AC_ARG_ENABLE([debug-context-memory-manager], + [AS_HELP_STRING([--enable-debug-context-memory-manager], + [use the debug context memory manager])]) -if test -z "${enable_context_memory_manager+set}"; then - enable_context_memory_manager=yes +if test -z "${enable_debug_context_memory_manager+set}"; then + enable_debug_context_memory_manager=no fi -AC_MSG_RESULT([$enable_context_memory_manager]) +AC_MSG_RESULT([$enable_debug_context_memory_manager]) -if test "$enable_context_memory_manager" = yes; then - CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_CONTEXT_MEMORY_MANAGER" +if test "$enable_debug_context_memory_manager" = yes; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER" fi AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4]) diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index a36d523f7..bbaf606ec 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -31,7 +31,7 @@ namespace CVC4 { namespace context { -#ifdef CVC4_CONTEXT_MEMORY_MANAGER +#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER void ContextMemoryManager::newChunk() { @@ -168,7 +168,7 @@ void ContextMemoryManager::pop() { } } -#endif /* CVC4_CONTEXT_MEMORY_MANAGER */ +#endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */ } /* CVC4::context namespace */ } /* CVC4 namespace */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index b7e5ec119..3607d97c3 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -27,7 +27,7 @@ namespace CVC4 { namespace context { -#ifdef CVC4_CONTEXT_MEMORY_MANAGER +#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER /** * Region-based memory manager for contexts. Calls to newData provide memory @@ -148,11 +148,14 @@ class ContextMemoryManager { };/* class ContextMemoryManager */ -#else /* CVC4_CONTEXT_MEMORY_MANAGER */ +#else /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */ + +#warning \ + "Using the debug version of ContextMemoryManager, expect performance degradation" /** * Dummy implementation of the ContextMemoryManager for debugging purposes. Use - * the configure flag "--disable-context-memory-manager" to use this + * the configure flag "--enable-debug-context-memory-manager" to use this * implementation. */ class ContextMemoryManager @@ -164,6 +167,16 @@ class ContextMemoryManager } ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); } + ~ContextMemoryManager() + { + for (const auto& levelAllocs : d_allocations) + { + for (auto alloc : levelAllocs) + { + free(alloc); + } + } + } void* newData(size_t size) { @@ -187,7 +200,7 @@ class ContextMemoryManager std::vector<std::vector<char*>> d_allocations; }; /* ContextMemoryManager */ -#endif /* CVC4_CONTEXT_MEMORY_MANAGER */ +#endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */ /** * An STL-like allocator class for allocating from context memory. |