diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/context | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/backtrackable.h | 2 | ||||
-rw-r--r-- | src/context/cdhashmap.h | 10 | ||||
-rw-r--r-- | src/context/cdhashset.h | 7 | ||||
-rw-r--r-- | src/context/cdinsert_hashmap.h | 5 | ||||
-rw-r--r-- | src/context/cdlist.h | 12 | ||||
-rw-r--r-- | src/context/cdo.h | 1 | ||||
-rw-r--r-- | src/context/cdqueue.h | 8 | ||||
-rw-r--r-- | src/context/cdtrail_queue.h | 2 | ||||
-rw-r--r-- | src/context/context.cpp | 32 | ||||
-rw-r--r-- | src/context/context.h | 12 | ||||
-rw-r--r-- | src/context/context_mm.cpp | 10 |
11 files changed, 50 insertions, 51 deletions
diff --git a/src/context/backtrackable.h b/src/context/backtrackable.h index 5d358941f..85281e7fa 100644 --- a/src/context/backtrackable.h +++ b/src/context/backtrackable.h @@ -160,7 +160,7 @@ template <class T> void List<T>::concat (List<T>* other) { bck->checkConsistency(); bck->notifyConcat(this, other); - Assert(tail->next==NULL); + Assert(tail->next == NULL); tail->next = other->head; Assert(other->ptr_to_head == NULL); other->ptr_to_head = tail; diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 05d68ead5..fc42c0e85 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -88,9 +88,9 @@ #include <unordered_map> #include <vector> -#include "base/cvc4_assert.h" -#include "context/context.h" +#include "base/check.h" #include "context/cdhashmap_forward.h" +#include "context/context.h" namespace CVC4 { namespace context { @@ -278,7 +278,11 @@ class CDHashMap : public ContextObj { Context* d_context; // Nothing to save; the elements take care of themselves - ContextObj* save(ContextMemoryManager* pCMM) override { Unreachable(); } + ContextObj* save(ContextMemoryManager* pCMM) override + { + Unreachable(); + SuppressWrongNoReturnWarning; + } // Similarly, nothing to restore void restore(ContextObj* data) override { Unreachable(); } diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index a35ecae88..57cd101a9 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -19,10 +19,9 @@ #ifndef CVC4__CONTEXT__CDHASHSET_H #define CVC4__CONTEXT__CDHASHSET_H -#include "base/cvc4_assert.h" -#include "context/context.h" +#include "base/check.h" #include "context/cdinsert_hashmap.h" - +#include "context/context.h" namespace CVC4 { namespace context { @@ -51,7 +50,7 @@ public: } static void operator delete(void* pMem) { - AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!"; } CDHashSet(Context* context) : diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index f15c418eb..0b3c713d2 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -38,13 +38,12 @@ #include <unordered_map> #include <utility> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" -#include "context/context.h" #include "context/cdinsert_hashmap_forward.h" +#include "context/context.h" #include "expr/node.h" - #pragma once namespace CVC4 { diff --git a/src/context/cdlist.h b/src/context/cdlist.h index dda88a0fd..95501df8e 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -25,10 +25,10 @@ #include <string> #include <sstream> -#include "base/cvc4_assert.h" +#include "base/check.h" +#include "context/cdlist_forward.h" #include "context/context.h" #include "context/context_mm.h" -#include "context/cdlist_forward.h" namespace CVC4 { namespace context { @@ -139,8 +139,8 @@ private: size_t newSize = GROWTH_FACTOR * d_sizeAlloc; if(newSize > d_allocator.max_size()) { newSize = d_allocator.max_size(); - Assert(newSize > d_sizeAlloc, - "cannot request larger list due to allocator limits"); + Assert(newSize > d_sizeAlloc) + << "cannot request larger list due to allocator limits"; } T* newList = d_allocator.allocate(newSize); Debug("cdlist") << "2x grow of cdlist " << this @@ -306,7 +306,7 @@ public: * Access to the ith item in the list. */ const T& operator[](size_t i) const { - Assert(i < d_size, "index out of bounds in CDList::operator[]"); + Assert(i < d_size) << "index out of bounds in CDList::operator[]"; return d_list[i]; } @@ -314,7 +314,7 @@ public: * Returns the most recent item added to the list. */ const T& back() const { - Assert(d_size > 0, "CDList::back() called on empty list"); + Assert(d_size > 0) << "CDList::back() called on empty list"; return d_list[d_size - 1]; } diff --git a/src/context/cdo.h b/src/context/cdo.h index fe588afb0..b7d32d856 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -19,7 +19,6 @@ #ifndef CVC4__CONTEXT__CDO_H #define CVC4__CONTEXT__CDO_H -#include "base/cvc4_assert.h" #include "context/context.h" diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index 6ad0e9339..079d2265c 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -125,21 +125,21 @@ public: * function. */ void pop(){ - Assert(!empty(), "Attempting to pop from an empty queue."); + Assert(!empty()) << "Attempting to pop from an empty queue."; ParentType::makeCurrent(); d_iter = d_iter + 1; if (empty() && d_lastsave != ParentType::d_size) { // Some elements have been enqueued and dequeued in the same // context and now the queue is empty we can destruct them. ParentType::truncateList(d_lastsave); - Assert(ParentType::d_size == d_lastsave); + Assert(ParentType::d_size == d_lastsave); d_iter = d_lastsave; } } /** Returns a reference to the next element on the queue. */ const T& front() const{ - Assert(!empty(), "No front in an empty queue."); + Assert(!empty()) << "No front in an empty queue."; return ParentType::d_list[d_iter]; } @@ -147,7 +147,7 @@ public: * Returns the most recent item added to the queue. */ const T& back() const { - Assert(!empty(), "CDQueue::back() called on empty list"); + Assert(!empty()) << "CDQueue::back() called on empty list"; return ParentType::d_list[ParentType::d_size - 1]; } diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h index ad2bef54c..4042c4223 100644 --- a/src/context/cdtrail_queue.h +++ b/src/context/cdtrail_queue.h @@ -74,7 +74,7 @@ public: /** Moves the iterator for the queue forward. */ void dequeue(){ - Assert(!empty(), "Attempting to queue from an empty queue."); + Assert(!empty()) << "Attempting to queue from an empty queue."; d_iter = d_iter + 1; } diff --git a/src/context/context.cpp b/src/context/context.cpp index 310f88b04..e1de944fe 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -18,7 +18,7 @@ #include <iostream> #include <vector> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/context.h" @@ -72,7 +72,7 @@ void Context::push() { void Context::pop() { - Assert(getLevel() > 0, "Cannot pop below level 0"); + Assert(getLevel() > 0) << "Cannot pop below level 0"; // Notify the (pre-pop) ContextNotifyObj objects ContextNotifyObj* pCNO = d_pCNOpre; @@ -149,11 +149,11 @@ void ContextObj::update() << *getContext() << std::endl; // Check that base class data was saved - Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext && - pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev && - pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore && - pContextObjSaved->d_pScope == d_pScope ), - "save() did not properly copy information in base class" ); + Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext + && pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev + && pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore + && pContextObjSaved->d_pScope == d_pScope)) + << "save() did not properly copy information in base class"; // Link the "saved" object in place of this ContextObj in the scope // we're moving it FROM. @@ -204,8 +204,8 @@ ContextObj* ContextObj::restoreAndContinue() // might not be bottom scope, since objects allocated in context // memory don't get linked to scope 0 // - // Assert(d_pScope == d_pScope->getContext()->getBottomScope(), - // "Expected bottom scope"); + // Assert(d_pScope == d_pScope->getContext()->getBottomScope()) << + // "Expected bottom scope"; Debug("context") << "NULL restore object! " << this << std::endl; pContextObjNext = d_pContextObjNext; @@ -270,8 +270,7 @@ ContextObj::ContextObj(Context* pContext) : d_pContextObjRestore(NULL), d_pContextObjNext(NULL), d_ppContextObjPrev(NULL) { - - Assert(pContext != NULL, "NULL context pointer"); + Assert(pContext != NULL) << "NULL context pointer"; Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl; d_pScope = pContext->getBottomScope(); @@ -284,8 +283,7 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) : d_pContextObjRestore(NULL), d_pContextObjNext(NULL), d_ppContextObjPrev(NULL) { - - Assert(pContext != NULL, "NULL context pointer"); + Assert(pContext != NULL) << "NULL context pointer"; Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl; if(allocatedInCMM) { @@ -341,16 +339,16 @@ std::ostream& operator<<(std::ostream& out, const Scope& scope) { out << "Scope " << scope.d_level << " [" << &scope << "]:"; ContextObj* pContextObj = scope.d_pContextObjList; - Assert(pContextObj == NULL || - pContextObj->prev() == &scope.d_pContextObjList); + Assert(pContextObj == NULL + || pContextObj->prev() == &scope.d_pContextObjList); while(pContextObj != NULL) { out << " <--> " << pContextObj; if(pContextObj->d_pScope != &scope) { out << " XXX bad scope" << std::endl; } Assert(pContextObj->d_pScope == &scope); - Assert(pContextObj->next() == NULL || - pContextObj->next()->prev() == &pContextObj->next()); + Assert(pContextObj->next() == NULL + || pContextObj->next()->prev() == &pContextObj->next()); pContextObj = pContextObj->next(); } return out << " --> NULL"; diff --git a/src/context/context.h b/src/context/context.h index d9d73f770..2bfc83a43 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -27,7 +27,7 @@ #include <typeinfo> #include <vector> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" #include "context/context_mm.h" @@ -135,10 +135,10 @@ public: } ~ScopedPush() noexcept(false) { d_context->pop(); - AlwaysAssert(d_context->getTopScope() == d_scope, - "Context::ScopedPush observed an uneven Context (at pop, " - "top scope doesn't match what it was at the time the " - "ScopedPush was applied)"); + AlwaysAssert(d_context->getTopScope() == d_scope) + << "Context::ScopedPush observed an uneven Context (at pop, " + "top scope doesn't match what it was at the time the " + "ScopedPush was applied)"; } };/* Context::ScopedPush */ @@ -569,7 +569,7 @@ class ContextObj { * calling deleteSelf(). */ static void operator delete(void* pMem) { - AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!"; } /** diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 76a2168d1..a9186f5f9 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -24,7 +24,7 @@ #include <valgrind/memcheck.h> #endif /* CVC4_VALGRIND */ -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" #include "context/context_mm.h" @@ -37,8 +37,8 @@ void ContextMemoryManager::newChunk() { // Increment index to chunk list ++d_indexChunkList; - Assert(d_chunkList.size() == d_indexChunkList, - "Index should be at the end of the list"); + Assert(d_chunkList.size() == d_indexChunkList) + << "Index should be at the end of the list"; // Create new chunk if no free chunk available if(d_freeChunks.empty()) { @@ -105,8 +105,8 @@ void* ContextMemoryManager::newData(size_t size) { newChunk(); res = (void*)d_nextFree; d_nextFree += size; - AlwaysAssert(d_nextFree <= d_endChunk, - "Request is bigger than memory chunk size"); + AlwaysAssert(d_nextFree <= d_endChunk) + << "Request is bigger than memory chunk size"; } Debug("context") << "ContextMemoryManager::newData(" << size << ") returning " << res << " at level " |