diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-02-08 18:36:12 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-08 18:36:12 -0800 |
| commit | 83f150c727f197c530d6f46a75b516eea52bed29 (patch) | |
| tree | 8c13925a1c572a7fce2c0f29b5c9b983bdcf6d92 /src/context/context_mm.cpp | |
| parent | 48d03da729c615114eae0e10d579ab5a58adec81 (diff) | |
Replace CMM flag with debug CMM flag, fix leak in debug CMM (#1586)
Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag
to use the context memory manager (which we want by default). This makes compiling with
other build systems cumbersome because you have to know about the flag.
This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER
flag that does the opposite (in absence of the flag, we use the context memory manager).
Additionally, the commit fixes a memory leak in the debug context memory manager (the
destructor did not clean up the allocations).
Diffstat (limited to 'src/context/context_mm.cpp')
| -rw-r--r-- | src/context/context_mm.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
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 */ |