Use -Wimplicit-fallthrough (#3464)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 18 Nov 2019 20:28:54 +0000 (12:28 -0800)
committerGitHub <noreply@github.com>
Mon, 18 Nov 2019 20:28:54 +0000 (12:28 -0800)
commit17f0468c1656aa91d7cc5e3174a797312a9364c3
tree0c765c27541a3d0eed0e10b2afc49613e5c719ef
parent6fe7877d82721e453d5d928a8fe9dbad2099dac1
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`).
13 files changed:
CMakeLists.txt
src/base/check.h
src/parser/smt2/smt2.cpp
src/preprocessing/passes/unconstrained_simplifier.cpp
src/printer/smt2/smt2_printer.cpp
src/proof/theory_proof.cpp
src/prop/cnf_stream.cpp
src/theory/arith/arith_rewriter.cpp
src/theory/arith/arith_static_learner.cpp
src/theory/arith/theory_arith_private.cpp
src/theory/uf/symmetry_breaker.cpp
src/util/sampler.cpp
test/unit/theory/theory_arith_white.h