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 ac12e2acb2d0cd7015c30fbeca2da998f187396e..916d6a6a1773e3c8618d22b98a4ded80bcfeaa6b 100644 (file)
--- 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 c0dbb3d7c2e86649931a909002fc4b746684f412..cc6bfb316fa65a2fed7360f1a34283dca2710047 100644 (file)
--- 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 ede5f5223ee581a3da2e8d18c13a7c3602526b61..7b43739aeaf6e1cbdc5b6153effb23930b43d97f 100644 (file)
--- a/src/include/cvc5_public.h
+++ b/src/include/cvc5_public.h
@@ -20,23 +20,29 @@
 #include <stddef.h>
 #include <stdint.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
+
+#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 9f59ad397876807cca5035ec964c3527e709df73..63f09d5537fb701da2cd66e6a94a8446d40602a9 100644 (file)
--- 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 a2cabb3a93d170fe79bcf4488971274c4b75aeb6..39324844e84a86853fa79c80d3e678634b987dc5 100644 (file)
--- 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<Node>& 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<Node>& 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 d01ec081ed332544d645e43ffb1032e31c21593d..feef06a90a3124dc22069beb93cb0b6fa72e5a3e 100644 (file)
--- 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 b75ebe288be05937d9a3b9420823e063b87e93ea..f505d27741244845bc7ee996b6e153fb52acac5b 100644 (file)
--- 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 a59ee5c5fdf6abf063016b331c1944477c1afd0b..ccda5fa77ec9d74c7bed39016f50898d92398b95 100644 (file)
--- 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 13e41978c0ebd0ce6090b858f67ee5d2f0777b5b..e2789a5b51bfb46e918814e6ff0c2fc9c3dc1b32 100644 (file)
--- 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 192b5dfc82944ed01a2958159be29ddbf1180c95..2b95829e0e1a4623bc9af40324b3ef115784d140 100644 (file)
--- 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 915b469dbb0351035b4cce8d50c2faeabc0e1991..eb80723fd53ef112da00e0855d576c7d10e6393b 100644 (file)
--- 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)