From aa00eacd101633c13cfe66743ba20c5fb4a264df Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 12:12:45 +0000 Subject: [PATCH 1/8] Revert "Change build system so that it always passes warning suppression flags" This reverts commit 4815a22b4e2bdc0648d6b208cf04bd5494318652. This isn't necessary anymore since the benchmarks in ldv-consumption have been fixed. --- c/Makefile.config | 49 +++++++++++++++++------------------------------ c/Makefile.rules | 13 ------------- 2 files changed, 18 insertions(+), 44 deletions(-) diff --git a/c/Makefile.config b/c/Makefile.config index b2948beb80e..309d6260bc8 100644 --- a/c/Makefile.config +++ b/c/Makefile.config @@ -81,49 +81,36 @@ WARNINGS_AS_ERRORS ?= 0 # Warning flags to be passed to clang and gcc (i.e. flags are supported by both # compilers). # -# COMMON_WARNINGS is only passed to the compiler if SUPPRESS_WARNINGS is 0 -# COMMON_WARNINGS_SUPPRESS is **ALWAYS** passed to the compiler -# # FIXME: Use of each -Wno-* flag NEEDS TO BE JUSTIFIED ################################################################################ -COMMON_WARNINGS := -Wall -COMMON_WARNINGS_SUPPRESS := -Wno-unused-label \ - -Wno-unused-function \ - -Wno-unused-variable \ - -Wno-unused-value \ - -Wno-unknown-pragmas \ - -Wno-attributes \ - -Wno-parentheses \ - -Wno-uninitialized \ - -Wno-pointer-to-int-cast \ - -Wno-int-to-pointer-cast \ - -Wno-pointer-sign \ - -Wno-return-type \ - -Wno-main \ - -Wno-sequence-point \ +COMMON_WARNINGS := -Wall \ + -Wno-unused-label \ + -Wno-unused-function \ + -Wno-unused-variable \ + -Wno-unused-value \ + -Wno-unknown-pragmas \ + -Wno-attributes \ + -Wno-parentheses \ + -Wno-uninitialized \ + -Wno-pointer-to-int-cast \ + -Wno-int-to-pointer-cast \ + -Wno-pointer-sign \ + -Wno-return-type \ + -Wno-main \ + -Wno-sequence-point \ ################################################################################ # Warning flags that will only be passed to gcc -# -# GCC_ONLY_WARNINGS is only passed to gcc if SUPPRESS_WARNINGS is 0 -# GCC_ONLY_WARNINGS_SUPPRESS is **ALWAYS** passed to the gcc -# # FIXME: Use of each -Wno-* flag NEEDS TO BE JUSTIFIED ################################################################################ -GCC_ONLY_WARNINGS := -GCC_ONLY_WARNINGS_SUPPRESS := -Wno-unused-but-set-variable \ - -Wno-maybe-uninitialized \ - -Wno-return-local-addr +GCC_ONLY_WARNINGS := -Wno-unused-but-set-variable \ + -Wno-maybe-uninitialized \ + -Wno-return-local-addr ################################################################################ # Warning flags that will only be passed to clang -# -# CLANG_ONLY_WARNINGS is only passed to clang if SUPPRESS_WARNINGS is 0 -# CLANG_ONLY_WARNINGS_SUPPRESS is **ALWAYS** passed to the clang -# ################################################################################ CLANG_ONLY_WARNINGS := -CLANG_ONLY_WARNINGS_SUPPRESS := ################################################################################ # Set default behaviour for suppressing compiler warnings diff --git a/c/Makefile.rules b/c/Makefile.rules index bac835de8ed..8c197e1078d 100644 --- a/c/Makefile.rules +++ b/c/Makefile.rules @@ -121,19 +121,6 @@ else CC.Warnings := -w endif -# FIXME: I don't like this but it seems to be necessary for Clang right now -# Warning suppression flags are always passed (regardless of SUPPRESS_WARNINGS) -# so that compilation can still pass (e.g. some benchmarks won't compile without -# -Wno-return-type with Clang) -CC.Warnings += $(COMMON_WARNINGS_SUPPRESS) -ifeq ($(CC_IS_GCC),1) - CC.Warnings += $(GCC_ONLY_WARNINGS_SUPPRESS) -else ifeq ($(CC_IS_CLANG),1) - CC.Warnings += $(CLANG_ONLY_WARNINGS_SUPPRESS) -else - $(error Compiler "$(CC)" was not identified as gcc or clang) -endif - CC.Flags += -std=$(CC.Standard) \ -m$(CC.Arch) \ $(CC.Warnings) \ From 6ab0e14f26fb11533bb7a306f1a55209f56dca30 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 12:26:16 +0000 Subject: [PATCH 2/8] Fix a benchmark that won't compile under Clang without ``-Wno-return-type``. --- ...v_main0_sequence_infinite_withcheck_stateful.cil.out.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c b/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c index 664af1a0c95..8321185d1c8 100644 --- a/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c +++ b/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c @@ -10129,7 +10129,7 @@ int main(void) #line 3678 ldv_check_final_state(); #line 3681 - return; + return 0; } } #line 3685 "/home/mikhail/launches/cpachecker-regression2/launcher-working-dir/ldv-manager-work-dir/work/current--X--drivers/isdn/hisax/hisax.ko--X--regression-testlinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/54/dscv_tempdir/dscv/ri/32_7a/drivers/isdn/hisax/config.c.prepared" @@ -76949,7 +76949,7 @@ static int hfcpci_empty_fifo_trans(struct BCState *bcs , bzfifo_type *bz , u_cha } } #line 481 "/home/mikhail/launches/cpachecker-regression2/launcher-working-dir/ldv-manager-work-dir/work/current--X--drivers/isdn/hisax/hisax.ko--X--regression-testlinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/54/dscv_tempdir/dscv/ri/32_7a/drivers/isdn/hisax/hfc_pci.c.prepared" -static int main_rec_hfcpci(struct BCState *bcs ) +static void main_rec_hfcpci(struct BCState *bcs ) { struct IsdnCardState *cs ; int rcnt ; @@ -80754,7 +80754,7 @@ static int receive_dmsg___0(struct IsdnCardState *cs ) } } #line 507 "/home/mikhail/launches/cpachecker-regression2/launcher-working-dir/ldv-manager-work-dir/work/current--X--drivers/isdn/hisax/hisax.ko--X--regression-testlinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/54/dscv_tempdir/dscv/ri/32_7a/drivers/isdn/hisax/hfc_sx.c.prepared" -static int main_rec_hfcsx(struct BCState *bcs ) +static void main_rec_hfcsx(struct BCState *bcs ) { struct IsdnCardState *cs ; int count ; @@ -80804,7 +80804,7 @@ static int main_rec_hfcsx(struct BCState *bcs ) } #line 532 - return 0; + return; } } #line 539 "/home/mikhail/launches/cpachecker-regression2/launcher-working-dir/ldv-manager-work-dir/work/current--X--drivers/isdn/hisax/hisax.ko--X--regression-testlinux-3.8-rc1--X--32_7a--X--cpachecker/linux-3.8-rc1/csd_deg_dscv/54/dscv_tempdir/dscv/ri/32_7a/drivers/isdn/hisax/hfc_sx.c.prepared" From 4f4c27e8219f2b5eb1d57829f9191c7e6bb3129a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 12:43:25 +0000 Subject: [PATCH 3/8] Introduce the concept of "warnings as errors" into the build system so that we can have certain warnings treated as errors. Now we no longer suppress -Wmain and instead pass -Werror=main so that incorrect main() functions trigger a compiler error instead of a warning. --- c/Makefile.config | 16 +++++++++++++++- c/Makefile.rules | 5 +++++ 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/c/Makefile.config b/c/Makefile.config index 309d6260bc8..3a79928f679 100644 --- a/c/Makefile.config +++ b/c/Makefile.config @@ -96,21 +96,35 @@ COMMON_WARNINGS := -Wall \ -Wno-int-to-pointer-cast \ -Wno-pointer-sign \ -Wno-return-type \ - -Wno-main \ -Wno-sequence-point \ +################################################################################ +# Warnings to be treated as errors. Unlike COMMON_WARNINGS and *_ONLY_WARNINGS +# these are always passed to be compiler, regardless of SUPPRESS_WARNINGS +################################################################################ +COMMON_WARNINGS_AS_ERRORS := -Werror=main + ################################################################################ # Warning flags that will only be passed to gcc # FIXME: Use of each -Wno-* flag NEEDS TO BE JUSTIFIED +# Note GCC_ONLY_WARNINGS_AS_ERRORS are warnings that should be treated as errors. +# Unlike GCC_ONLY_WARNINGS, GCC_ONLY_WARNINGS_AS_ERRORS is always passed to the +# compiler regardless of SUPPRESS_WARNINGS ################################################################################ GCC_ONLY_WARNINGS := -Wno-unused-but-set-variable \ -Wno-maybe-uninitialized \ -Wno-return-local-addr +GCC_ONLY_WARNINGS_AS_ERRORS := ################################################################################ # Warning flags that will only be passed to clang +# Note CLANG_ONLY_WARNINGS_AS_ERRORS are warnings that should be treated as errors. +# Unlike CLANG_ONLY_WARNINGS, CLANG_ONLY_WARNINGS_AS_ERRORS is always passed to the +# compiler regardless of SUPPRESS_WARNINGS ################################################################################ CLANG_ONLY_WARNINGS := +CLANG_ONLY_WARNINGS_AS_ERRORS := + ################################################################################ # Set default behaviour for suppressing compiler warnings diff --git a/c/Makefile.rules b/c/Makefile.rules index 8c197e1078d..39cf09c6d7e 100644 --- a/c/Makefile.rules +++ b/c/Makefile.rules @@ -108,8 +108,10 @@ ifeq ($(SUPPRESS_WARNINGS),0) ifeq ($(CC_IS_GCC),1) CC.Warnings += $(GCC_ONLY_WARNINGS) + CC.Flags += $(GCC_ONLY_WARNINGS_AS_ERRORS) else ifeq ($(CC_IS_CLANG),1) CC.Warnings += $(CLANG_ONLY_WARNINGS) + CC.Flags += $(CLANG_ONLY_WARNINGS_AS_ERRORS) else $(error Compiler "$(CC)" was not identified as gcc or clang) endif @@ -121,6 +123,9 @@ else CC.Warnings := -w endif +# Warnings as errors are always passed to the compiler +CC.Flags += $(COMMON_WARNINGS_AS_ERRORS) + CC.Flags += -std=$(CC.Standard) \ -m$(CC.Arch) \ $(CC.Warnings) \ From be1e71f4f53eef2207772ed95f06192b5d779acf Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 12:56:27 +0000 Subject: [PATCH 4/8] Fix a benchmark is ldv-races that would not compile under Clang without -Wno-return-type --- c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.c | 4 ++-- c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.i | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.c b/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.c index 2d5f41d3d2d..5f835296f66 100644 --- a/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.c +++ b/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.c @@ -31,7 +31,7 @@ void *thread_ath9k(void *arg) { } } exit_thread_ath9k: - return; + return 0; } int ieee80211_register_hw(void) { @@ -104,7 +104,7 @@ void *thread_usb(void *arg) { //not a race pdev = 9; ldv_assert(pdev==9); - return; + return 0; } diff --git a/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.i b/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.i index e715a827798..f4322a6254e 100644 --- a/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.i +++ b/c/ldv-races/race-4_2-thread_local_vars_false-unreach-call.i @@ -4094,7 +4094,7 @@ void *thread_ath9k(void *arg) { } } exit_thread_ath9k: - return; + return 0; } int ieee80211_register_hw(void) { @@ -4167,7 +4167,7 @@ exit_thread_usb: pdev = 9; ldv_assert(pdev==9); - return; + return 0; } From 78eeac25567e1c010c61cfd5a90f0287ce293748 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 13:02:58 +0000 Subject: [PATCH 5/8] Fix benchmark in loop-invgen that won't compile with Clang without -Wno-return-type --- c/loop-invgen/apache-escape-absolute_true-unreach-call.c | 2 +- c/loop-invgen/apache-escape-absolute_true-unreach-call.i | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/c/loop-invgen/apache-escape-absolute_true-unreach-call.c b/c/loop-invgen/apache-escape-absolute_true-unreach-call.c index 5a60fdce4b7..254ce9548ae 100644 --- a/c/loop-invgen/apache-escape-absolute_true-unreach-call.c +++ b/c/loop-invgen/apache-escape-absolute_true-unreach-call.c @@ -65,5 +65,5 @@ int main() } END: - return; + return 0; } diff --git a/c/loop-invgen/apache-escape-absolute_true-unreach-call.i b/c/loop-invgen/apache-escape-absolute_true-unreach-call.i index a7e0dc8222a..1e9d11b7195 100644 --- a/c/loop-invgen/apache-escape-absolute_true-unreach-call.i +++ b/c/loop-invgen/apache-escape-absolute_true-unreach-call.i @@ -65,5 +65,5 @@ int main() } } END: - return; + return 0; } From 1471f9a75c3672bd6245b104eae72fd4b59cb7dc Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 13:05:04 +0000 Subject: [PATCH 6/8] Do not suppress -Wreturn-type. Doing so is not justifiable as it is a good indicator of bad code. --- c/Makefile.config | 1 - 1 file changed, 1 deletion(-) diff --git a/c/Makefile.config b/c/Makefile.config index 3a79928f679..8a1a286bb20 100644 --- a/c/Makefile.config +++ b/c/Makefile.config @@ -95,7 +95,6 @@ COMMON_WARNINGS := -Wall \ -Wno-pointer-to-int-cast \ -Wno-int-to-pointer-cast \ -Wno-pointer-sign \ - -Wno-return-type \ -Wno-sequence-point \ ################################################################################ From d93bec44a48169d54a3fc2fb051d6460199ab8fe Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 13:07:01 +0000 Subject: [PATCH 7/8] Do not suppress -Wuninitialized . Suppressing this warning is not justifiable as it likely means there is undefined behaviour. --- c/Makefile.config | 1 - 1 file changed, 1 deletion(-) diff --git a/c/Makefile.config b/c/Makefile.config index 8a1a286bb20..f94c00b0e76 100644 --- a/c/Makefile.config +++ b/c/Makefile.config @@ -91,7 +91,6 @@ COMMON_WARNINGS := -Wall \ -Wno-unknown-pragmas \ -Wno-attributes \ -Wno-parentheses \ - -Wno-uninitialized \ -Wno-pointer-to-int-cast \ -Wno-int-to-pointer-cast \ -Wno-pointer-sign \ From 508a4a79fa1c142c4a10e149d85faf8d636a4b31 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 4 Nov 2015 13:25:41 +0000 Subject: [PATCH 8/8] Add a note about using -Werror=implicit-function-declaration and -Werror=implicit-int. I tried adding these but the benchmarks don't compile with these set and it looks like a lot of work to fix these. --- c/Makefile.config | 1 + 1 file changed, 1 insertion(+) diff --git a/c/Makefile.config b/c/Makefile.config index f94c00b0e76..3ff6a611631 100644 --- a/c/Makefile.config +++ b/c/Makefile.config @@ -100,6 +100,7 @@ COMMON_WARNINGS := -Wall \ # Warnings to be treated as errors. Unlike COMMON_WARNINGS and *_ONLY_WARNINGS # these are always passed to be compiler, regardless of SUPPRESS_WARNINGS ################################################################################ +# TODO: Add -Werror=implicit-function-declaration and -Werror=implicit-int COMMON_WARNINGS_AS_ERRORS := -Werror=main ################################################################################