From 520e4a0638675dad2fa66a50e5fd64786c6f889f Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Wed, 2 Nov 2016 16:55:37 -0700 Subject: Fix back() of empty deque in context_mm_black test The `testPushPop()` test case does a pop out of scope at the end that lead to UB in `ContextManager::pop()` because it did a `deque::back()` on an empty deque without checking. This commit adds an assertion in the `ContextManager` and checks that the test case triggers the assertion. --- src/context/context_mm.cpp | 2 ++ test/unit/context/context_mm_black.h | 5 ++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 2dc2c03bb..ac7d7f8cf 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -104,6 +104,8 @@ void ContextMemoryManager::push() { void ContextMemoryManager::pop() { + Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0); + // Restore state from stack d_nextFree = d_nextFreeStack.back(); d_nextFreeStack.pop_back(); diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 60671653c..00a0fd05f 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -20,8 +20,11 @@ //Used in some of the tests #include #include + #include "context/context_mm.h" +#include "base/cvc4_assert.h" + using namespace std; using namespace CVC4::context; @@ -87,7 +90,7 @@ public: } // Try popping out of scope - d_cmm->pop(); + TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException); } void tearDown() { -- cgit v1.2.3