Use -Wimplicit-fallthrough (#3464)

This commit enables compiler warnings for implicit fallthroughs in
switch statements that are not explicitly marked as such. The commit
introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate
that a fallthrough is intentional. The commit fixes existing warnings
and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't
be triggered easily because we rewrite `abs` to an `ite` while expanding
definitions).

To have the new macro also available in the parser, the commit changes
`src/base/check.h` to be visible to the parser (it includes
`cvc4_private_library.h` now instead of `cvc4_private.h`).

4 files changed, 20 insertions, 20 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index c95d6f53d..13ab03b45 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -197,6 +197,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
                                  NodeManager::currentNM()->mkConst(-rat));
         }
       }
+      return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
       return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::TO_INTEGER:
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index e17605ead..810eded82 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -252,25 +252,23 @@ void ArithStaticLearner::addBound(TNode n) {
   DeltaRational bound = constant;
 
   switch(Kind k = n.getKind()) {
-  case kind::LT:
-    bound = DeltaRational(constant, -1);
-    /* fall through */
-  case kind::LEQ:
-    if (maxFind == d_maxMap.end() || (*maxFind).second > bound) {
-      d_maxMap.insert(n[0], bound);
-      Debug("arith::static") << "adding bound " << n << endl;
-    }
-    break;
-  case kind::GT:
-    bound = DeltaRational(constant, 1);
-    /* fall through */
-  case kind::GEQ:
-    if (minFind == d_minMap.end() || (*minFind).second < bound) {
-      d_minMap.insert(n[0], bound);
-      Debug("arith::static") << "adding bound " << n << endl;
-    }
-    break;
-  default: Unhandled() << k; break;
+    case kind::LT: bound = DeltaRational(constant, -1); CVC4_FALLTHROUGH;
+    case kind::LEQ:
+      if (maxFind == d_maxMap.end() || (*maxFind).second > bound)
+      {
+        d_maxMap.insert(n[0], bound);
+        Debug("arith::static") << "adding bound " << n << endl;
+      }
+      break;
+    case kind::GT: bound = DeltaRational(constant, 1); CVC4_FALLTHROUGH;
+    case kind::GEQ:
+      if (minFind == d_minMap.end() || (*minFind).second < bound)
+      {
+        d_minMap.insert(n[0], bound);
+        Debug("arith::static") << "adding bound " << n << endl;
+      }
+      break;
+    default: Unhandled() << k; break;
   }
 }
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 62be1fcc1..a6a47c73c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -5392,6 +5392,7 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith
       }
       // intentionally fall through to DISTINCT case!
       // entailments of negations are eager exit cases for EQUAL
+      CVC4_FALLTHROUGH;
     case DISTINCT:
       if(!bestPrimDiff.first.isNull()){
         // primDir [dm * dp] <= primDir * dm * U < primDir * sep
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 56d0c59cc..49ceebfd6 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -370,7 +370,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) {
         Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
       }
     }
-    /* intentional fall-through! */
+    CVC4_FALLTHROUGH;
   case kind::XOR:
     // commutative binary operator handling
     return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n);