diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-30 19:00:23 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-30 19:00:23 -0800 |
| commit | 6d740ab8167fe0f48ea78306d65e2cb8a4de2d09 (patch) | |
| tree | 55af24ca0024a7a5327b936213c055eca96107cf /test | |
| parent | 4c1f1cad720a94226f7834874cf59478de35b74a (diff) | |
Add debugging tools for ContextMemoryManager (#1407)
This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:
--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.
--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/context/context_mm_black.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 2fcc30e7b..c789702f5 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -40,7 +40,7 @@ public: } void testPushPop() { - +#ifdef CVC4_CONTEXT_MEMORY_MANAGER // Push, then allocate, then pop // We make sure that we don't allocate too much so that all the regions // should be reclaimed @@ -91,6 +91,9 @@ public: // Try popping out of scope TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException); +#else /* CVC4_CONTEXT_MEMORY_MANAGER */ +#warning "Context memory manager disabled, omitting unit tests" +#endif /* __CVC4__CONTEXT__CONTEXT_MM_H */ } void tearDown() { |