diff options
| -rw-r--r-- | src/context/cdlist_context_memory.h | 2 | ||||
| -rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
| -rw-r--r-- | src/expr/node_manager.h | 2 | ||||
| -rw-r--r-- | src/include/cvc4_public.h | 10 | ||||
| -rw-r--r-- | src/theory/output_channel.h | 4 | ||||
| -rw-r--r-- | src/util/options.h | 4 |
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 { |