added experimental "make lcov" target (it runs only unit tests); better coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes

4 files changed, 32 insertions, 29 deletions

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index b0161c562..a2abc08d8 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -95,6 +95,7 @@ private:
   CDList(const CDList<T>& l) :
     ContextObj(l),
     d_list(NULL),
+    d_callDestructor(l.d_callDestructor),
     d_size(l.d_size),
     d_sizeAlloc(0) {
   }
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 75f6eb2ae..4621d7fc5 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -140,24 +140,6 @@ public:
   }
 };/* class CDOmap<> */
 
-// Dummy subclass of ContextObj to serve as our data class
-class CDMapData : public ContextObj {
-  // befriend CDMap<> so that it can allocate us
-  template <class Key, class Data, class HashFcn>
-  friend class CDMap;
-
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDMapData(*this);
-  }
-
-  void restore(ContextObj* data) {}
-
-public:
-
-  CDMapData(Context* context) : ContextObj(context) {}
-  CDMapData(const ContextObj& co) : ContextObj(co) {}
-  ~CDMapData() throw(AssertionException) { destroy(); }
-};
 
 /**
  * Generic templated class for a map which must be saved and restored
@@ -181,11 +163,13 @@ class CDMap : public ContextObj {
 
   // Nothing to save; the elements take care of themselves
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDMapData(*this);
+    Unreachable();
   }
 
   // Similarly, nothing to restore
-  virtual void restore(ContextObj* data) {}
+  virtual void restore(ContextObj* data) {
+    Unreachable();
+  }
 
   void emptyTrash() {
     //FIXME multithreading
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 96152d075..fda2801be 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -199,7 +199,6 @@ inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValu
     if(x->d_nchildren == 1) {
       Assert(y->d_nchildren == 0);
       return compare(y, x);
-      return *reinterpret_cast<T*>(x->d_children[0]) == y->getConst<T>();
     } else if(y->d_nchildren == 1) {
       Assert(x->d_nchildren == 0);
       return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
diff --git a/src/util/output.h b/src/util/output.h
index 6315389e8..79bdd788e 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -172,8 +172,8 @@ class CVC4_PUBLIC NoticeC {
 public:
   NoticeC(std::ostream* os) : d_os(os) {}
 
-  void operator()(const char*);
-  void operator()(std::string);
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
@@ -193,8 +193,8 @@ class CVC4_PUBLIC ChatC {
 public:
   ChatC(std::ostream* os) : d_os(os) {}
 
-  void operator()(const char*);
-  void operator()(std::string);
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
@@ -215,10 +215,29 @@ class CVC4_PUBLIC TraceC {
 public:
   TraceC(std::ostream* os) : d_os(os) {}
 
-  void operator()(const char* tag, const char*);
-  void operator()(const char* tag, std::string);
-  void operator()(std::string tag, const char*);
-  void operator()(std::string tag, std::string);
+  void operator()(const char* tag, const char* s) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
+
+  void operator()(const char* tag, const std::string& s) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
+
+  void operator()(const std::string& tag, const char* s) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
+
+  void operator()(const std::string& tag, const std::string& s) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
 
   void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
   void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));