diff options
| -rw-r--r-- | src/context/cdhashmap.h | 20 | ||||
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 2 | ||||
| -rw-r--r-- | src/options/options_template.cpp | 6 | ||||
| -rw-r--r-- | src/proof/theory_proof.cpp | 4 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 1 |
5 files changed, 14 insertions, 19 deletions
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index d080da333..884234eb8 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -163,7 +163,7 @@ class CDOhash_map : public ContextObj { d_data = p->d_data; } } - // Explicitly call destructors fro the key and the date as they will not + // Explicitly call destructors for the key and the date as they will not // otherwise get called. p->d_key.~Key(); p->d_data.~Data(); @@ -478,18 +478,13 @@ public: typename table_type::iterator i = d_map.find(k); if(i != d_map.end()) { Debug("gc") << "key " << k << " obliterated" << std::endl; - // We can't call ->deleteSelf() here, because it calls the - // ContextObj destructor, which calls CDOhash_map::destroy(), which - // restore()'s, which puts the CDOhash_map on the trash, which causes - // a double-delete. - (*i).second->~Element(); - // Writing ...->~CDOhash_map() in the above is legal (?) but breaks - // g++ 4.1, though later versions have no problem. + // Restore this object to level 0. If it was inserted after level 0, + // nothing else to do as restore will put it in the trash. + (*i).second->destroy(); + // Check if object was inserted at level 0: in that case, still have + // to do some work. typename table_type::iterator j = d_map.find(k); - // This if() succeeds for objects inserted when in the - // zero-scope: they were never save()'d there, so restore() - // never gets a NULL map and so they leak. if(j != d_map.end()) { Element* elt = (*j).second; if(d_first == elt) { @@ -505,9 +500,8 @@ public: } d_map.erase(j);//FIXME multithreading Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl; - // was already destructed, so don't call ->deleteSelf() if(!elt->d_noTrash) { - ::operator delete(elt); + elt->deleteSelf(); } } } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index ef74575f3..53e16751e 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -30,7 +30,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 33 "${template}" +#line 34 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index f029dfd17..694d46d31 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -720,7 +720,7 @@ void Options::parseOptionsRecursive(Options* options, switch(c) { ${all_modules_option_handlers} -#line 722 "${template}" +#line 724 "${template}" case ':': // This can be a long or short option, and the way to get at the @@ -798,7 +798,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 800 "${template}" +#line 802 "${template}" NULL };/* smtOptions[] */ @@ -820,7 +820,7 @@ std::vector< std::vector<std::string> > Options::getOptions() const throw() { ${all_modules_get_options} -#line 762 "${template}" +#line 824 "${template}" return opts; } diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 634b2b738..a000bb8b3 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -620,7 +620,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } } - Assert(found); + AlwaysAssert(found); Debug("pf::tp") << "Replacing theory assertion " << clause_expr[k] << " with " @@ -729,7 +729,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } } - Assert(found); + AlwaysAssert(found); Debug("pf::tp") << "Replacing theory assertion " << currentClauseExpr[k] diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 6615d6b37..9d934a6e0 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -34,6 +34,7 @@ UNIT_TESTS += \ context/cdo_black \ context/cdlist_black \ context/cdlist_context_memory_black \ + context/cdmap_black \ context/cdmap_white \ context/cdvector_black \ context/stacking_vector_black \ |