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

1 files changed, 10 insertions, 0 deletions

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))