Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,

re-enabled cdmap_black.

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index d080da333a110078b06d3406689c311acdc2f956..884234eb8c031788c8ed32aef0ed04fab193ed42 100644 (file)
--- 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 ef74575f3de7cbb329966a5bda69769592b37402..53e16751e119538ccf5a109b90b66a9069b434c2 100644 (file)
--- 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 f029dfd176b7fbe60bc2d860812eee71cdecf267..694d46d312ade0f67943fe7ed18191d563e2b1ab 100644 (file)
--- 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 634b2b73829abf34100de9a9cd398360d97f6d53..a000bb8b36f6feb5745287285d9e135fc512e9e2 100644 (file)
--- 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 6615d6b37c173bf6d9191c1dea3d3da1aeab4e70..9d934a6e06ab723bcd91570fe31a20f295ceee4d 100644 (file)
--- 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 \