summaryrefslogtreecommitdiff
path: root/CMakeLists.txt
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-11-18 12:28:54 -0800
committerGitHub <noreply@github.com>2019-11-18 12:28:54 -0800
commit17f0468c1656aa91d7cc5e3174a797312a9364c3 (patch)
tree0c765c27541a3d0eed0e10b2afc49613e5c719ef /CMakeLists.txt
parent6fe7877d82721e453d5d928a8fe9dbad2099dac1 (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 'CMakeLists.txt')
-rw-r--r--CMakeLists.txt1
1 files changed, 1 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index fbdd05c95..c2ce3e6ac 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -189,6 +189,7 @@ add_check_c_flag("-fexceptions")
add_check_c_cxx_flag("-Wno-deprecated")
add_check_cxx_flag("-Wsuggest-override")
add_check_cxx_flag("-Wnon-virtual-dtor")
+add_check_c_cxx_flag("-Wimplicit-fallthrough")
# Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
# cdlist.h warnings. Remove when fixed.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback