From: Morgan Deters Date: Sun, 24 Oct 2010 02:44:35 +0000 (+0000) Subject: add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like private... X-Git-Tag: cvc5-1.0.0~8782 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8a8f335f4043a0117f2b92af3d1e94f285e4d30;p=cvc5.git 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 --- 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& l); + CDList(const CDList& 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 #include -#include "exception.h" -#include "language.h" +#include "util/exception.h" +#include "util/language.h" namespace CVC4 {