diff --git a/c/Makefile.config b/c/Makefile.config index b2948beb80e..3ff6a611631 100644 --- a/c/Makefile.config +++ b/c/Makefile.config @@ -81,49 +81,49 @@ 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-pointer-to-int-cast \ + -Wno-int-to-pointer-cast \ + -Wno-pointer-sign \ + -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 +################################################################################ +# TODO: Add -Werror=implicit-function-declaration and -Werror=implicit-int +COMMON_WARNINGS_AS_ERRORS := -Werror=main ################################################################################ # 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 +# 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 := -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 +GCC_ONLY_WARNINGS_AS_ERRORS := ################################################################################ # 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 -# +# 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_SUPPRESS := +CLANG_ONLY_WARNINGS_AS_ERRORS := + ################################################################################ # Set default behaviour for suppressing compiler warnings diff --git a/c/Makefile.rules b/c/Makefile.rules index bac835de8ed..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,18 +123,8 @@ 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 +# Warnings as errors are always passed to the compiler +CC.Flags += $(COMMON_WARNINGS_AS_ERRORS) CC.Flags += -std=$(CC.Standard) \ -m$(CC.Arch) \ 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" 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; } 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; }