add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like private...

diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h
index f85d3b79ebe44d6f0f747cffa2da54eaf2f29844..20d672d31a32c630eb0750c490d18dc19d869218 100644 (file)
--- 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 7946a734ec5839e42ef13e517ea377b69386dac9..4577135970056bca02a5b743a80a899ad0c66170 100644 (file)
--- 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 d434799b7f3ab04ab3d43dcf2202f223954a966b..6c7bf500bbcc7ee810637bf7524b6124bb6f62a7 100644 (file)
--- 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 714c32e298c30a49f082c469e865edeb97868a07..f2dbd3bce0567f348b105b75c0f1e583c221352c 100644 (file)
--- 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 cc51c7a7c4dafe11084f23fbfd6282559d14845e..1c48c0160d5724da36a066016fda1bccde3340b8 100644 (file)
--- 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 e232176b57df468e520a0966b8f9fa5a8f430ea8..a7e9c8a2a8a75bd79ca2eb15d3d2ed21ed60fab6 100644 (file)
--- 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 {