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/parser | |
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/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ae0607b53..b693eae5b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -15,6 +15,9 @@ **/ #include "parser/smt2/smt2.h" +#include <algorithm> + +#include "base/check.h" #include "expr/type.h" #include "options/options.h" #include "parser/antlr_input.h" @@ -23,8 +26,6 @@ #include "printer/sygus_print_callback.h" #include "util/bitvector.h" -#include <algorithm> - // ANTLR defines these, which is really bad! #undef true #undef false @@ -303,6 +304,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::IS_INTEGER, "is_int"); addOperator(kind::TO_REAL, "to_real"); // falling through on purpose, to add Ints part of Reals_Ints + CVC4_FALLTHROUGH; case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); |