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`).

1 files changed, 6 insertions, 18 deletions

diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
index eeb38f988..60d38bb34 100644
--- a/src/util/sampler.cpp
+++ b/src/util/sampler.cpp
@@ -73,37 +73,27 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s)
 
       // +/- inf
       // sign = x, exp = 11...11, sig = 00...00
-      case 1:
-        sign = one;
-        // Intentional fall-through
+      case 1: sign = one; CVC4_FALLTHROUGH;
       case 2: exp = BitVector::mkOnes(e); break;
 
       // +/- zero
       // sign = x, exp = 00...00, sig = 00...00
-      case 3:
-        sign = one;
-        // Intentional fall-through
+      case 3: sign = one; CVC4_FALLTHROUGH;
       case 4: break;
 
       // +/- max subnormal
       // sign = x, exp = 00...00, sig = 11...11
-      case 5:
-        sign = one;
-        // Intentional fall-through
+      case 5: sign = one; CVC4_FALLTHROUGH;
       case 6: sig = BitVector::mkOnes(s - 1); break;
 
       // +/- min subnormal
       // sign = x, exp = 00...00, sig = 00...01
-      case 7:
-        sign = one;
-        // Intentional fall-through
+      case 7: sign = one; CVC4_FALLTHROUGH;
       case 8: sig = BitVector(s - 1, static_cast<unsigned int>(1)); break;
 
       // +/- max normal
       // sign = x, exp = 11...10, sig = 11...11
-      case 9:
-        sign = one;
-        // Intentional fall-through
+      case 9: sign = one; CVC4_FALLTHROUGH;
       case 10:
         exp = BitVector::mkOnes(e) - BitVector(e, static_cast<unsigned int>(1));
         sig = BitVector::mkOnes(s - 1);
@@ -111,9 +101,7 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s)
 
       // +/- min normal
       // sign = x, exp = 00...01, sig = 00...00
-      case 11:
-        sign = one;
-        // Intentional fall-through
+      case 11: sign = one; CVC4_FALLTHROUGH;
       case 12: exp = BitVector(e, static_cast<unsigned int>(1)); break;
 
       default: Unreachable();