add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like private copy constructors and assignment, for instance) that generates better, compile-time error messages if the function is used (before, you'd have to wait until link time); also some minor cleanup

6 files changed, 17 insertions, 7 deletions

diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h
index f85d3b79e..20d672d31 100644
--- a/src/context/cdlist_context_memory.h
+++ b/src/context/cdlist_context_memory.h
@@ -157,7 +157,7 @@ protected:
   /**
    * Private copy constructor undefined (no copy permitted).
    */
-  CDList(const CDList<T, Allocator>& l);
+  CDList(const CDList<T, Allocator>& l) CVC4_UNDEFINED;
 
   /**
    * Allocate the first list segment.
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 7946a734e..457713597 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -75,7 +75,7 @@ private:
   friend class ExprManagerScope;
 
   // undefined, private copy constructor (disallow copy)
-  ExprManager(const ExprManager&);
+  ExprManager(const ExprManager&) CVC4_UNDEFINED;
 
 public:
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d434799b7..6c7bf500b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -240,7 +240,7 @@ class NodeManager {
   // bool properlyContainsDecision(TNode); // all children are atomic
 
   // undefined private copy constructor (disallow copy)
-  NodeManager(const NodeManager&);
+  NodeManager(const NodeManager&) CVC4_UNDEFINED;
 
 public:
 
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index 714c32e29..f2dbd3bce 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -45,6 +45,16 @@
 #  endif /* __GNUC__ >= 4 */
 #endif /* defined _WIN32 || defined __CYGWIN__ */
 
+// Can use CVC4_UNDEFINED for things like undefined, private
+// copy constructors.  The advantage is that with CVC4_UNDEFINED,
+// if something _does_ try to call the function, you get an error
+// at the point of the call (rather than a link error later).
+#ifdef __GNUC__
+#  define CVC4_UNDEFINED __attribute__((error("this function intentionally undefined")))
+#else /* ! __GNUC__ */
+#  define CVC4_UNDEFINED
+#endif /* __GNUC__ */
+
 #define EXPECT_TRUE(x) __builtin_expect( (x), true )
 #define EXPECT_FALSE(x) __builtin_expect( (x), false )
 #define NORETURN __attribute__ ((noreturn))
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index cc51c7a7c..1c48c0160 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -32,10 +32,10 @@ namespace theory {
  */
 class OutputChannel {
   /** Disallow copying: private constructor */
-  OutputChannel(const OutputChannel&);
+  OutputChannel(const OutputChannel&) CVC4_UNDEFINED;
 
   /** Disallow assignment: private operator=() */
-  OutputChannel& operator=(const OutputChannel&);
+  OutputChannel& operator=(const OutputChannel&) CVC4_UNDEFINED;
 
 public:
 
diff --git a/src/util/options.h b/src/util/options.h
index e232176b5..a7e9c8a2a 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -36,8 +36,8 @@
 #include <iostream>
 #include <string>
 
-#include "exception.h"
-#include "language.h"
+#include "util/exception.h"
+#include "util/language.h"
 
 namespace CVC4 {