diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-18 12:28:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-18 12:28:54 -0800 |
commit | 17f0468c1656aa91d7cc5e3174a797312a9364c3 (patch) | |
tree | 0c765c27541a3d0eed0e10b2afc49613e5c719ef /src/theory | |
parent | 6fe7877d82721e453d5d928a8fe9dbad2099dac1 (diff) |
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`).
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 1 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 36 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 1 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 2 |
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); |