From: Andres Notzli <andres.noetzli@gmail.com>
Date: Wed, 2 Nov 2016 23:55:37 +0000 (-0700)
Subject: Fix back() of empty deque in context_mm_black test
X-Git-Tag: cvc5-1.0.0~6006^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=520e4a0638675dad2fa66a50e5fd64786c6f889f;p=cvc5.git

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 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 <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() {