From: Andres Noetzli Date: Fri, 10 Sep 2021 02:58:42 +0000 (-0700) Subject: Use C++17 attributes (#7154) X-Git-Tag: cvc5-1.0.0~1239 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6255b7045c9e21066eb48cead218e44f7add5826;p=cvc5.git Use C++17 attributes (#7154) Currently, we are using non-standard attributes. With C++17, all the attributes that we use regularly are now standardized. This commit replaces the compiler-specific attributes with standard ones. --- diff --git a/src/base/check.h b/src/base/check.h index ac12e2acb..916d6a6a1 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -39,30 +39,6 @@ #include "base/exception.h" #include "cvc5_export.h" -// Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be -// false (if there is compiler support). -#ifdef __has_builtin -#if __has_builtin(__builtin_expect) -#define CVC5_PREDICT_FALSE(x) (__builtin_expect(x, false)) -#define CVC5_PREDICT_TRUE(x) (__builtin_expect(x, true)) -#else -#define CVC5_PREDICT_FALSE(x) x -#define CVC5_PREDICT_TRUE(x) x -#endif -#else -#define CVC5_PREDICT_FALSE(x) x -#define CVC5_PREDICT_TRUE(x) x -#endif - -#ifdef __has_cpp_attribute -#if __has_cpp_attribute(fallthrough) -#define CVC5_FALLTHROUGH [[fallthrough]] -#endif // __has_cpp_attribute(fallthrough) -#endif // __has_cpp_attribute -#ifndef CVC5_FALLTHROUGH -#define CVC5_FALLTHROUGH -#endif - namespace cvc5 { // Implementation notes: diff --git a/src/base/output.h b/src/base/output.h index c0dbb3d7c..cc6bfb316 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -469,10 +469,10 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT; // just parenthesize it e.g. !(Debug("foo").isOn()) class __cvc5_true { - void operator!() CVC5_UNUSED; - void operator~() CVC5_UNUSED; - void operator-() CVC5_UNUSED; - void operator+() CVC5_UNUSED; + CVC5_UNUSED void operator!(); + CVC5_UNUSED void operator~(); + CVC5_UNUSED void operator-(); + CVC5_UNUSED void operator+(); public: inline operator bool() { return true; } diff --git a/src/include/cvc5_public.h b/src/include/cvc5_public.h index ede5f5223..7b43739ae 100644 --- a/src/include/cvc5_public.h +++ b/src/include/cvc5_public.h @@ -20,23 +20,29 @@ #include #include +// Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be +// false (if there is compiler support). +#ifdef __has_builtin +#if __has_builtin(__builtin_expect) +#define CVC5_PREDICT_FALSE(x) (__builtin_expect(x, false)) +#define CVC5_PREDICT_TRUE(x) (__builtin_expect(x, true)) +#else +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x +#endif +#else +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x +#endif + +#define CVC5_FALLTHROUGH [[fallthrough]] + // CVC5_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__ -#define CVC5_UNUSED __attribute__((__unused__)) -#define CVC5_NORETURN __attribute__((__noreturn__)) -#define CVC5_CONST_FUNCTION __attribute__((__const__)) -#define CVC5_PURE_FUNCTION __attribute__((__pure__)) -#define CVC5_WARN_UNUSED_RESULT __attribute__((__warn_unused_result__)) -#else /* ! __GNUC__ */ -#define CVC5_UNUSED -#define CVC5_NORETURN -#define CVC5_CONST_FUNCTION -#define CVC5_PURE_FUNCTION -#define CVC5_WARN_UNUSED_RESULT -#endif /* __GNUC__ */ +#define CVC5_UNUSED [[maybe_unused]] +#define CVC5_NORETURN [[noreturn]] +#define CVC5_WARN_UNUSED_RESULT [[nodiscard]] #endif /* CVC5_PUBLIC_H */ diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 9f59ad397..63f09d553 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -1456,7 +1456,7 @@ uint32_t countReachable(TNode x, Kind k) Node ITESimplifier::simpITEAtom(TNode atom) { - static int CVC5_UNUSED instance = 0; + CVC5_UNUSED static int instance = 0; Debug("ite::atom") << "still simplifying " << (++instance) << endl; Node attempt = transformAtom(atom); Debug("ite::atom") << " finished " << instance << endl; diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index a2cabb3a9..39324844e 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -36,9 +36,8 @@ class BooleanSimplification { BooleanSimplification() = delete; BooleanSimplification(const BooleanSimplification&) = delete; - static bool push_back_associative_commute_recursive( - Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) - CVC5_WARN_UNUSED_RESULT; + CVC5_WARN_UNUSED_RESULT static bool push_back_associative_commute_recursive( + Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode); public: /** diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index d01ec081e..feef06a90 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -99,7 +99,7 @@ class CircuitPropagator * @return a trust node encapsulating the proof for a conflict as a lemma that * proves false, or the null trust node otherwise */ - TrustNode propagate() CVC5_WARN_UNUSED_RESULT; + CVC5_WARN_UNUSED_RESULT TrustNode propagate(); /** * Get the back edges of this circuit. diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index b75ebe288..f505d2774 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -154,8 +154,8 @@ class TermTupleEnumeratorBase : public TermTupleEnumeratorInterface /** Set up terms for given variable. */ virtual size_t prepareTerms(size_t variableIx) = 0; /** Get a given term for a given variable. */ - virtual Node getTerm(size_t variableIx, - size_t term_index) CVC5_WARN_UNUSED_RESULT = 0; + CVC5_WARN_UNUSED_RESULT virtual Node getTerm(size_t variableIx, + size_t term_index) = 0; }; /** diff --git a/src/theory/theory.h b/src/theory/theory.h index a59ee5c5f..ccda5fa77 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -440,18 +440,7 @@ class Theory : protected EnvObj EFFORT_LAST_CALL = 200 }; /* enum Effort */ - static inline bool standardEffortOrMore(Effort e) CVC5_CONST_FUNCTION - { - return e >= EFFORT_STANDARD; - } - static inline bool standardEffortOnly(Effort e) CVC5_CONST_FUNCTION - { - return e >= EFFORT_STANDARD && e < EFFORT_FULL; - } - static inline bool fullEffort(Effort e) CVC5_CONST_FUNCTION - { - return e == EFFORT_FULL; - } + static bool fullEffort(Effort e) { return e == EFFORT_FULL; } /** * Get the id for this Theory. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 13e41978c..e2789a5b5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -695,7 +695,7 @@ void TheoryEngine::postsolve() { d_inSatMode = false; // Reset the interrupt flag d_interrupted = false; - bool CVC5_UNUSED wasInConflict = d_inConflict; + CVC5_UNUSED bool wasInConflict = d_inConflict; try { // Definition of the statement that is to be run by every theory diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 192b5dfc8..2b95829e0 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -151,7 +151,7 @@ public: * differ from the input due to theory-rewriting and preprocessing, * as well as CNF conversion */ - Node ensureLiteral(TNode n) CVC5_WARN_UNUSED_RESULT; + CVC5_WARN_UNUSED_RESULT Node ensureLiteral(TNode n); /** * This returns the theory-preprocessed form of term n. The theory diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index 915b469db..eb80723fd 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -61,14 +61,8 @@ TEST_F(TestTheoryWhite, effort) Theory::Effort s = Theory::EFFORT_STANDARD; Theory::Effort f = Theory::EFFORT_FULL; - ASSERT_TRUE(Theory::standardEffortOnly(s)); - ASSERT_FALSE(Theory::standardEffortOnly(f)); - ASSERT_FALSE(Theory::fullEffort(s)); ASSERT_TRUE(Theory::fullEffort(f)); - - ASSERT_TRUE(Theory::standardEffortOrMore(s)); - ASSERT_TRUE(Theory::standardEffortOrMore(f)); } TEST_F(TestTheoryWhite, done)