From d09bb1889f184de32ceb078a815e016502e24279 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 1 Sep 2016 01:28:02 -0700 Subject: Relaxing the throw specifiers for the destructors for Node, TypeNode, the context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes. --- src/context/cdchunk_list.h | 4 ++-- src/context/cdhashmap.h | 4 ++-- src/context/cdinsert_hashmap.h | 2 +- src/context/cdlist.h | 2 +- src/context/cdo.h | 2 +- src/context/cdtrail_hashmap.h | 2 +- src/context/context.cpp | 4 ++-- src/context/context.h | 10 +++++----- src/context/context_mm.cpp | 2 +- src/context/context_mm.h | 4 ++-- src/context/stacking_vector.h | 2 +- src/expr/node.h | 4 ++-- src/expr/type_node.h | 4 ++-- src/prop/bvminisat/bvminisat.cpp | 4 +--- src/prop/bvminisat/bvminisat.h | 2 +- src/prop/cryptominisat.cpp | 2 +- src/prop/cryptominisat.h | 6 +----- src/prop/minisat/minisat.cpp | 2 +- src/prop/minisat/minisat.h | 2 +- src/prop/sat_solver.h | 4 ++-- src/theory/bv/bv_inequality_graph.h | 2 +- src/theory/shared_terms_database.cpp | 2 +- src/theory/shared_terms_database.h | 2 +- src/theory/uf/equality_engine.cpp | 2 +- src/theory/uf/equality_engine.h | 2 +- 25 files changed, 36 insertions(+), 42 deletions(-) diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h index 3fa3c6b5d..e75f4de4d 100644 --- a/src/context/cdchunk_list.h +++ b/src/context/cdchunk_list.h @@ -137,7 +137,7 @@ protected: d_size(size), d_sizeAlloc(sizeAlloc) { } - ~CDChunkListSave() throw() { + ~CDChunkListSave() { this->destroy(); } ContextObj* save(ContextMemoryManager* pCMM) { @@ -322,7 +322,7 @@ public: /** * Destructor: delete the list */ - ~CDChunkList() throw(AssertionException) { + ~CDChunkList() { this->destroy(); if(this->d_callDestructor) { diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 884234eb8..6ae74fbde 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -236,7 +236,7 @@ public: } } - ~CDOhash_map() throw(AssertionException) { + ~CDOhash_map() { destroy(); } @@ -327,7 +327,7 @@ public: d_trash() { } - ~CDHashMap() throw(AssertionException) { + ~CDHashMap() { Debug("gc") << "cdhashmap" << this << " disappearing, destroying..." << std::endl; destroy(); diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index 6e772068b..e901e9413 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -271,7 +271,7 @@ public: /** * Destructor: delete the d_insertMap */ - ~CDInsertHashMap() throw(AssertionException) { + ~CDInsertHashMap() { this->destroy(); delete d_insertMap; } diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 4e42c4688..4a5ebfd30 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -257,7 +257,7 @@ public: /** * Destructor: delete the list */ - ~CDList() throw(AssertionException) { + ~CDList() { this->destroy(); if(this->d_callDestructor) { diff --git a/src/context/cdo.h b/src/context/cdo.h index e2fdcf9bd..21465181c 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -140,7 +140,7 @@ public: /** * Destructor - call destroy() method */ - ~CDO() throw(AssertionException) { destroy(); } + ~CDO() { destroy(); } /** * Set the data in the CDO. First call makeCurrent. diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h index e89c1b528..90816d542 100644 --- a/src/context/cdtrail_hashmap.h +++ b/src/context/cdtrail_hashmap.h @@ -452,7 +452,7 @@ public: /** * Destructor: delete the map */ - ~CDTrailHashMap() throw(AssertionException) { + ~CDTrailHashMap() { this->destroy(); delete d_trailMap; } diff --git a/src/context/context.cpp b/src/context/context.cpp index 9c0416ce8..8f151ad08 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -35,7 +35,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) { } -Context::~Context() throw(AssertionException) { +Context::~Context() { // Delete all Scopes popto(0); @@ -306,7 +306,7 @@ ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) { } -ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) { +ContextNotifyObj::~ContextNotifyObj() { if(d_pCNOnext != NULL) { d_pCNOnext->d_ppCNOprev = d_ppCNOprev; } diff --git a/src/context/context.h b/src/context/context.h index 4f45e8954..f7707bdec 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -152,7 +152,7 @@ public: /** * Destructor: pop all scopes, delete ContextMemoryManager */ - ~Context() throw(AssertionException); + ~Context(); /** * Return the current (top) scope @@ -277,7 +277,7 @@ public: * Destructor: Restore all of the objects in ContextObjList. Defined inline * below. */ - ~Scope() throw(AssertionException); + ~Scope(); /** * Get the Context for this Scope @@ -615,7 +615,7 @@ public: /** * Destructor does nothing: subclass must explicitly call destroy() instead. */ - virtual ~ContextObj() throw(AssertionException) {} + virtual ~ContextObj() {} /** * If you want to allocate a ContextObj object on the heap, use this @@ -711,7 +711,7 @@ public: /** * Destructor: removes object from list */ - virtual ~ContextNotifyObj() throw(AssertionException); + virtual ~ContextNotifyObj(); };/* class ContextNotifyObj */ @@ -725,7 +725,7 @@ inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) { update(); } -inline Scope::~Scope() throw(AssertionException) { +inline Scope::~Scope() { // Call restore() method on each ContextObj object in the list. // Note that it is the responsibility of restore() to return the // next item in the list. diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 0a6b08b6a..2dc2c03bb 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -63,7 +63,7 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) { } -ContextMemoryManager::~ContextMemoryManager() throw() { +ContextMemoryManager::~ContextMemoryManager() { // Delete all chunks while(!d_chunkList.empty()) { free(d_chunkList.back()); diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 99b448cf2..673fb9098 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -118,7 +118,7 @@ public: /** * Destructor - deletes all memory in all regions */ - ~ContextMemoryManager() throw(); + ~ContextMemoryManager(); /** * Allocate size bytes from the current region @@ -161,7 +161,7 @@ public: ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {} template ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.getCMM()) {} - ~ContextMemoryAllocator() throw() {} + ~ContextMemoryAllocator() {} ContextMemoryManager* getCMM() const { return d_mm; } T* address(T& v) const { return &v; } diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h index b737c40ae..4b482c9b0 100644 --- a/src/context/stacking_vector.h +++ b/src/context/stacking_vector.h @@ -50,7 +50,7 @@ public: d_offset(ctxt, 0) { } - ~StackingVector() throw() { } + ~StackingVector() { } /** * Return a value from the vector. If n is not a key in diff --git a/src/expr/node.h b/src/expr/node.h index 998294da3..c9bfb75a4 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -308,7 +308,7 @@ public: * Destructor. If ref_count is true it will decrement the reference count * and, if zero, collect the NodeValue. */ - ~NodeTemplate() throw(AssertionException); + ~NodeTemplate(); /** * Return the null node. @@ -1089,7 +1089,7 @@ NodeTemplate::NodeTemplate(const Expr& e) { } template -NodeTemplate::~NodeTemplate() throw(AssertionException) { +NodeTemplate::~NodeTemplate() { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); if(ref_count) { // shouldn't ever fail diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 46fdaa143..0cada0df2 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -116,7 +116,7 @@ public: * Destructor. If ref_count is true it will decrement the reference count * and, if zero, collect the NodeValue. */ - ~TypeNode() throw(AssertionException); + ~TypeNode(); /** * Assignment operator for nodes, copies the relevant information from node @@ -785,7 +785,7 @@ inline TypeNode::TypeNode(const TypeNode& typeNode) { d_nv->inc(); } -inline TypeNode::~TypeNode() throw(AssertionException) { +inline TypeNode::~TypeNode() { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); d_nv->dec(); } diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 54e3f2e8b..368a79b80 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -39,7 +39,7 @@ BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Co } -BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) { +BVMinisatSatSolver::~BVMinisatSatSolver() { delete d_minisat; delete d_minisatNotify; } @@ -309,5 +309,3 @@ void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_ } } - - diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 56a7c61e2..732bd0313 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -72,7 +72,7 @@ protected: public: BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); - ~BVMinisatSatSolver() throw(AssertionException); + virtual ~BVMinisatSatSolver(); void setNotify(Notify* notify); diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index d8f25a786..eff079cc9 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -45,7 +45,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, } -CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) { +CryptoMinisatSolver::~CryptoMinisatSolver() { delete d_solver; } diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index 54d52af0e..7ad861def 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -38,7 +38,7 @@ private: public: CryptoMinisatSolver(StatisticsRegistry* registry, const std::string& name = ""); - ~CryptoMinisatSolver() throw(AssertionException); + virtual ~CryptoMinisatSolver(); ClauseId addClause(SatClause& clause, bool removable); ClauseId addXorClause(SatClause& clause, bool rhs, bool removable); @@ -132,7 +132,3 @@ public: } // CVC4 #endif // CVC4_USE_CRYPTOMINISAT - - - - diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ff726e299..a88a872c8 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -38,7 +38,7 @@ MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) : d_statistics(registry) {} -MinisatSatSolver::~MinisatSatSolver() throw() +MinisatSatSolver::~MinisatSatSolver() { delete d_minisat; } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ec5297bb7..1627a6575 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -29,7 +29,7 @@ class MinisatSatSolver : public DPLLSatSolverInterface { public: MinisatSatSolver(StatisticsRegistry* registry); - ~MinisatSatSolver() throw(); + virtual ~MinisatSatSolver(); ; static SatVariable toSatVariable(Minisat::Var var); diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 81fb94242..4afaea5a0 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -43,7 +43,7 @@ class SatSolver { public: /** Virtual destructor */ - virtual ~SatSolver() throw(AssertionException) { } + virtual ~SatSolver() { } /** Assert a clause in the solver. */ virtual ClauseId addClause(SatClause& clause, @@ -99,7 +99,7 @@ public: class BVSatSolverInterface: public SatSolver { public: - virtual ~BVSatSolverInterface() throw(AssertionException) {} + virtual ~BVSatSolverInterface() {} /** Interface for notifications */ class Notify { public: diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 452172586..923e1d8c5 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -242,7 +242,7 @@ public: */ bool addDisequality(TNode a, TNode b, TNode reason); void getConflict(std::vector& conflict); - virtual ~InequalityGraph() throw(AssertionException) {} + virtual ~InequalityGraph() {} /** * Check that the currently asserted disequalities that have not been split on * are still true in the current model. diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 0dc6cc7a1..b78109dfb 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -37,7 +37,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } -SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) +SharedTermsDatabase::~SharedTermsDatabase() { smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index c108122ef..cc8959165 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -149,7 +149,7 @@ private: public: SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context); - ~SharedTermsDatabase() throw(AssertionException); + ~SharedTermsDatabase(); /** * Asserts the equality to the shared terms database, diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 09d348584..f98ad556f 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -97,7 +97,7 @@ void EqualityEngine::init() { d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS; } -EqualityEngine::~EqualityEngine() throw(AssertionException) { +EqualityEngine::~EqualityEngine() { free(d_triggerDatabase); } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 843e7ce7f..18e83bd1a 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -186,7 +186,7 @@ public: /** * Just a destructor. */ - virtual ~EqualityEngine() throw(AssertionException); + virtual ~EqualityEngine(); /** * Set the master equality engine for this one. Master engine will get copies of all -- cgit v1.2.3