From c831d34205a473cbace8a546704a992ba8220dd6 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 7 Aug 2018 17:26:58 -0700 Subject: [PATCH] Delete functions instead of using CVC4_UNDEFINED (#1794) C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable. --- .travis.yml | 2 +- config/bindings.m4 | 2 +- src/api/cvc4cpp.h | 4 ++-- src/base/exception.h | 4 ++-- src/base/listener.h | 9 ++++----- src/context/cdhashmap.h | 6 +++--- src/context/cdhashset.h | 4 ++-- src/context/cdinsert_hashmap.h | 2 +- src/context/cdlist.h | 2 +- src/context/cdo.h | 2 +- src/context/context.h | 8 ++++---- src/expr/expr_manager_template.h | 4 ++-- src/expr/node_manager.h | 4 ++-- src/include/cvc4_public.h | 16 ---------------- src/main/portfolio_util.h | 4 ++-- src/options/options.h | 4 ++-- src/parser/antlr_input.h | 5 ++--- src/parser/input.h | 4 ++-- src/printer/printer.h | 4 ++-- src/prop/bvminisat/bvminisat.h | 2 +- src/smt/smt_engine.h | 4 ++-- src/smt_util/boolean_simplification.h | 4 ++-- src/smt_util/lemma_channels.h | 4 ++-- src/theory/rewriter.h | 4 ++-- src/theory/theory.h | 6 +++--- src/util/bin_heap.h | 4 ++-- src/util/resource_manager.h | 4 ++-- src/util/statistics_registry.h | 10 +++++----- 28 files changed, 57 insertions(+), 75 deletions(-) diff --git a/.travis.yml b/.travis.yml index d1f72f955..27cb2915b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,7 +32,7 @@ addons: - libgmp-dev - libboost-dev - libboost-thread-dev - - swig + - swig3.0 - libcln-dev - openjdk-7-jdk - antlr3 diff --git a/config/bindings.m4 b/config/bindings.m4 index 7174934c1..5941d81cd 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -47,7 +47,7 @@ if test "$noswig" = yes; then SWIG= else if test -z "$SWIG"; then - AC_CHECK_PROGS(SWIG, [swig swig2.0 swig-2], [], []) + AC_CHECK_PROGS(SWIG, [swig swig3.0 swig-3], [], []) else AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", []) fi diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index c3c429009..0d05c9b19 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1303,8 +1303,8 @@ class CVC4_PUBLIC Solver /** * Disallow copy/assignment. */ - Solver(const Solver&) CVC4_UNDEFINED; - Solver& operator=(const Solver&) CVC4_UNDEFINED; + Solver(const Solver&) = delete; + Solver& operator=(const Solver&) = delete; /* .................................................................... */ /* Sorts Handling */ diff --git a/src/base/exception.h b/src/base/exception.h index c6619ddd6..983a59572 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -158,8 +158,8 @@ public: private: /* Disallow copies */ - LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNDEFINED; - LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNDEFINED; + LastExceptionBuffer(const LastExceptionBuffer&) = delete; + LastExceptionBuffer& operator=(const LastExceptionBuffer&) = delete; char* d_contents; diff --git a/src/base/listener.h b/src/base/listener.h index 7e8d00039..88bcee742 100644 --- a/src/base/listener.h +++ b/src/base/listener.h @@ -125,14 +125,14 @@ private: * The user of the class must be know to remove listeners on the collection. * Allowing copies will only cause confusion. */ - ListenerCollection(const ListenerCollection& copy) CVC4_UNDEFINED; + ListenerCollection(const ListenerCollection& copy) = delete; /** * Disabling the assignment operator. * The user of the class must be know to remove listeners on the collection. * Allowing copies will only cause confusion. */ - ListenerCollection& operator=(const ListenerCollection& copy) CVC4_UNDEFINED; + ListenerCollection& operator=(const ListenerCollection& copy) = delete; /** A list of the listeners in the collection.*/ ListenerList d_listeners; @@ -153,10 +153,9 @@ class ListenerRegistrationList { private: /** Disallow copying.*/ - ListenerRegistrationList(const ListenerRegistrationList&) CVC4_UNDEFINED; + ListenerRegistrationList(const ListenerRegistrationList&) = delete; /** Disallow assignment.*/ - ListenerRegistrationList operator=(const ListenerRegistrationList&) - CVC4_UNDEFINED; + ListenerRegistrationList operator=(const ListenerRegistrationList&) = delete; std::list d_registrations; };/* class CVC4::ListenerRegistrationList */ diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 94b507a7e..958c48e22 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -177,7 +177,7 @@ class CDOhash_map : public ContextObj { d_next(NULL) { } - CDOhash_map& operator=(const CDOhash_map&) CVC4_UNDEFINED; + CDOhash_map& operator=(const CDOhash_map&) = delete; public: CDOhash_map(Context* context, @@ -290,8 +290,8 @@ class CDHashMap : public ContextObj { void restore(ContextObj* data) override { Unreachable(); } // no copy or assignment - CDHashMap(const CDHashMap&) CVC4_UNDEFINED; - CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED; + CDHashMap(const CDHashMap&) = delete; + CDHashMap& operator=(const CDHashMap&) = delete; public: CDHashMap(Context* context) diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index 0dc1f087d..b907d9823 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -32,8 +32,8 @@ class CDHashSet : protected CDInsertHashMap { typedef CDInsertHashMap super; // no copy or assignment - CDHashSet(const CDHashSet&) CVC4_UNDEFINED; - CDHashSet& operator=(const CDHashSet&) CVC4_UNDEFINED; + CDHashSet(const CDHashSet&) = delete; + CDHashSet& operator=(const CDHashSet&) = delete; public: diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index 62268b471..d59bf584d 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -214,7 +214,7 @@ private: << " from " << &l << " size " << d_size << std::endl; } - CDInsertHashMap& operator=(const CDInsertHashMap&) CVC4_UNDEFINED; + CDInsertHashMap& operator=(const CDInsertHashMap&) = delete; /** * Implementation of mandatory ContextObj method save: simply copies diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 8fcc977af..834e363f9 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -113,7 +113,7 @@ protected: << " from " << &l << " size " << d_size << std::endl; } - CDList& operator=(const CDList& l) CVC4_UNDEFINED; + CDList& operator=(const CDList& l) = delete; private: /** diff --git a/src/context/cdo.h b/src/context/cdo.h index 3cb646d6c..da6c8d338 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -50,7 +50,7 @@ protected: /** * operator= for CDO is private to ensure CDO object is not copied. */ - CDO& operator=(const CDO& cdo) CVC4_UNDEFINED; + CDO& operator=(const CDO& cdo) = delete; /** * Implementation of mandatory ContextObj method save: simply copies the diff --git a/src/context/context.h b/src/context/context.h index acff2b5c2..04da9c25d 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -94,8 +94,8 @@ class Context { friend std::ostream& operator<<(std::ostream&, const Context&); // disable copy, assignment - Context(const Context&) CVC4_UNDEFINED; - Context& operator=(const Context&) CVC4_UNDEFINED; + Context(const Context&) = delete; + Context& operator=(const Context&) = delete; public: @@ -208,8 +208,8 @@ public: class UserContext : public Context { private: // disable copy, assignment - UserContext(const UserContext&) CVC4_UNDEFINED; - UserContext& operator=(const UserContext&) CVC4_UNDEFINED; + UserContext(const UserContext&) = delete; + UserContext& operator=(const UserContext&) = delete; public: UserContext() {} };/* class UserContext */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index a9cdfc587..bce1c8940 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -83,8 +83,8 @@ private: friend class NodeManager; // undefined, private copy constructor and assignment op (disallow copy) - ExprManager(const ExprManager&) CVC4_UNDEFINED; - ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; + ExprManager(const ExprManager&) = delete; + ExprManager& operator=(const ExprManager&) = delete; std::vector d_keep_dtt; std::vector d_keep_dt; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 71082ef9d..f7f3fb144 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -349,9 +349,9 @@ class NodeManager { // bool properlyContainsDecision(TNode); // all children are atomic // undefined private copy constructor (disallow copy) - NodeManager(const NodeManager&) CVC4_UNDEFINED; + NodeManager(const NodeManager&) = delete; - NodeManager& operator=(const NodeManager&) CVC4_UNDEFINED; + NodeManager& operator=(const NodeManager&) = delete; void init(); diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index e1d406b03..7950a5af6 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -31,27 +31,11 @@ # 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). - // CVC4_UNUSED is to mark something (e.g. local variable, function) // as being _possibly_ unused, so that the compiler generates no // warning about it. This might be the case for e.g. a variable // only used in DEBUG builds. -#ifdef __GNUC__ -# if __GNUC__ > 4 || ( __GNUC__ == 4 && __GNUC_MINOR__ >= 3 ) - /* error function attribute only exists in GCC >= 4.3.0 */ -# define CVC4_UNDEFINED __attribute__((__error__("this function intentionally undefined"))) -# else /* GCC < 4.3.0 */ -# define CVC4_UNDEFINED -# endif /* GCC >= 4.3.0 */ -#else /* ! __GNUC__ */ -# define CVC4_UNDEFINED -#endif /* __GNUC__ */ - #ifdef __GNUC__ # define CVC4_UNUSED __attribute__((__unused__)) # define CVC4_NORETURN __attribute__ ((__noreturn__)) diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index ab65cbaf0..6ebd97d3d 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -86,8 +86,8 @@ class OptionsList { size_t size() const; private: - OptionsList(const OptionsList&) CVC4_UNDEFINED; - OptionsList& operator=(const OptionsList&) CVC4_UNDEFINED; + OptionsList(const OptionsList&) = delete; + OptionsList& operator=(const OptionsList&) = delete; std::vector d_options; }; diff --git a/src/options/options.h b/src/options/options.h index 8ca713642..16210e1a3 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -114,13 +114,13 @@ class CVC4_PUBLIC Options { * Options cannot be copied as they are given an explicit list of * Listeners to respond to. */ - Options(const Options& options) CVC4_UNDEFINED; + Options(const Options& options) = delete; /** * Options cannot be assigned as they are given an explicit list of * Listeners to respond to. */ - Options& operator=(const Options& options) CVC4_UNDEFINED; + Options& operator=(const Options& options) = delete; static std::string formatThreadOptionException(const std::string& option); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 3a0c0fdfe..5598dd359 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -69,11 +69,10 @@ private: LineBuffer* line_buffer); /* This is private and unimplemented, because you should never use it. */ - AntlrInputStream(const AntlrInputStream& inputStream) CVC4_UNDEFINED; + AntlrInputStream(const AntlrInputStream& inputStream) = delete; /* This is private and unimplemented, because you should never use it. */ - AntlrInputStream& operator=(const AntlrInputStream& inputStream) - CVC4_UNDEFINED; + AntlrInputStream& operator=(const AntlrInputStream& inputStream) = delete; public: diff --git a/src/parser/input.h b/src/parser/input.h index 4f1a0f7da..02d92749d 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -90,8 +90,8 @@ class CVC4_PUBLIC Input { * copy construction and assignment. Mark them private and do not define * them. */ - Input(const Input& input) CVC4_UNDEFINED; - Input& operator=(const Input& input) CVC4_UNDEFINED; + Input(const Input& input) = delete; + Input& operator=(const Input& input) = delete; public: /** Create an input for the given file. diff --git a/src/printer/printer.h b/src/printer/printer.h index 29d4f5598..6b34094e7 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -100,8 +100,8 @@ class Printer private: /** Disallow copy, assignment */ - Printer(const Printer&) CVC4_UNDEFINED; - Printer& operator=(const Printer&) CVC4_UNDEFINED; + Printer(const Printer&) = delete; + Printer& operator=(const Printer&) = delete; /** Make a Printer for a given OutputLanguage */ static std::unique_ptr makePrinter(OutputLanguage lang); diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 6578b5ee8..728d26bd4 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -121,7 +121,7 @@ public: private: /* Disable the default constructor. */ - BVMinisatSatSolver() CVC4_UNDEFINED; + BVMinisatSatSolver() = delete; class Statistics { public: diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e4bd7d77d..dc5a5e703 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -402,8 +402,8 @@ class CVC4_PUBLIC SmtEngine { void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations"); // disallow copy/assignment - SmtEngine(const SmtEngine&) CVC4_UNDEFINED; - SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED; + SmtEngine(const SmtEngine&) = delete; + SmtEngine& operator=(const SmtEngine&) = delete; //check satisfiability (for query and check-sat) Result checkSatisfiability(const Expr& assumption, diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index 6274d0dbd..8e4d8aa25 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -35,8 +35,8 @@ namespace CVC4 { */ class BooleanSimplification { // cannot construct one of these - BooleanSimplification() CVC4_UNDEFINED; - BooleanSimplification(const BooleanSimplification&) CVC4_UNDEFINED; + BooleanSimplification() = delete; + BooleanSimplification(const BooleanSimplification&) = delete; static bool push_back_associative_commute_recursive( Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) diff --git a/src/smt_util/lemma_channels.h b/src/smt_util/lemma_channels.h index 67de37ed8..b2af0dfe4 100644 --- a/src/smt_util/lemma_channels.h +++ b/src/smt_util/lemma_channels.h @@ -60,10 +60,10 @@ class CVC4_PUBLIC LemmaChannels { private: // Disable copy constructor. - LemmaChannels(const LemmaChannels&) CVC4_UNDEFINED; + LemmaChannels(const LemmaChannels&) = delete; // Disable assignment operator. - LemmaChannels& operator=(const LemmaChannels&) CVC4_UNDEFINED; + LemmaChannels& operator=(const LemmaChannels&) = delete; /** This captures the old options::lemmaInputChannel .*/ LemmaInputChannel* d_lemmaInputChannel; diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index eda5dcf26..cc948ae7c 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -72,8 +72,8 @@ class Rewriter { TNode node, TNode cache); // disable construction of rewriters; all functionality is static - Rewriter() CVC4_UNDEFINED; - Rewriter(const Rewriter&) CVC4_UNDEFINED; + Rewriter() = delete; + Rewriter(const Rewriter&) = delete; /** * Rewrites the node using the given theory rewriter. diff --git a/src/theory/theory.h b/src/theory/theory.h index 2c3c727cb..5d176a36b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -83,9 +83,9 @@ private: friend class ::CVC4::TheoryEngine; // Disallow default construction, copy, assignment. - Theory() CVC4_UNDEFINED; - Theory(const Theory&) CVC4_UNDEFINED; - Theory& operator=(const Theory&) CVC4_UNDEFINED; + Theory() = delete; + Theory(const Theory&) = delete; + Theory& operator=(const Theory&) = delete; /** An integer identifying the type of the theory. */ TheoryId d_id; diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index 7d733829b..d547530b1 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -60,8 +60,8 @@ private: CmpFcn d_cmp; // disallow copy and assignment - BinaryHeap(const BinaryHeap&) CVC4_UNDEFINED; - BinaryHeap& operator=(const BinaryHeap&) CVC4_UNDEFINED; + BinaryHeap(const BinaryHeap&) = delete; + BinaryHeap& operator=(const BinaryHeap&) = delete; public: BinaryHeap(const CmpFcn& c = CmpFcn()) diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 2fa7a6bb4..3ca2babcf 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -120,13 +120,13 @@ class CVC4_PUBLIC ResourceManager { * ResourceManagers cannot be copied as they are given an explicit * list of Listeners to respond to. */ - ResourceManager(const ResourceManager&) CVC4_UNDEFINED; + ResourceManager(const ResourceManager&) = delete; /** * ResourceManagers cannot be assigned as they are given an explicit * list of Listeners to respond to. */ - ResourceManager& operator=(const ResourceManager&) CVC4_UNDEFINED; + ResourceManager& operator=(const ResourceManager&) = delete; public: diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index b000e91e8..d7f105b65 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -392,9 +392,9 @@ class WrappedStat : public ReadOnlyDataStat { const ReadOnlyDataStat& d_stat; /** Private copy constructor undefined (no copy permitted). */ - WrappedStat(const WrappedStat&) CVC4_UNDEFINED; + WrappedStat(const WrappedStat&) = delete; /** Private assignment operator undefined (no copy permitted). */ - WrappedStat& operator=(const WrappedStat&) CVC4_UNDEFINED; + WrappedStat& operator=(const WrappedStat&) = delete; public: @@ -653,7 +653,7 @@ class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat { private: /** Private copy constructor undefined (no copy permitted). */ - StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; + StatisticsRegistry(const StatisticsRegistry&) = delete; public: @@ -760,9 +760,9 @@ class CodeTimer { bool d_reentrant; /** Private copy constructor undefined (no copy permitted). */ - CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; + CodeTimer(const CodeTimer& timer) = delete; /** Private assignment operator undefined (no copy permitted). */ - CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; + CodeTimer& operator=(const CodeTimer& timer) = delete; public: CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) { -- 2.30.2