diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-02 16:55:37 -0700 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-02 17:09:55 -0700 |
commit | 520e4a0638675dad2fa66a50e5fd64786c6f889f (patch) | |
tree | 008e517455ecfcdfa3d25a17d2ba73a9638d0593 /test/unit | |
parent | f1427165156dff24d7b8ca0690088e4182ccdbd4 (diff) |
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.
Diffstat (limited to 'test/unit')
-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 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() { |