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.

diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 2dc2c03bb778fc5ced7fe9dff59bca845117abd6..ac7d7f8cf4f7eaee451ef1861cc0b560cccae06d 100644 (file)
--- 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 60671653c58b0d3ef244c1dcd5a86e707f290930..00a0fd05f821fe7733b64136b4f64c32ed48cf8b 100644 (file)
--- 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 <vector>
 #include <iostream>
+
 #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() {