From 6d740ab8167fe0f48ea78306d65e2cb8a4de2d09 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 30 Nov 2017 19:00:23 -0800 Subject: 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. --- test/unit/context/context_mm_black.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'test/unit/context') 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() { -- cgit v1.2.3