Remove some warning suppression flags and lay the ground work for treating some warnings as errors

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

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) \

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"

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;
 }
 
 

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;
 }
 
 

c/loop-invgen/apache-escape-absolute_true-unreach-call.c

@@ -65,5 +65,5 @@ int main()
     }
 
 END:
-    return;
+    return 0;
 }

c/loop-invgen/apache-escape-absolute_true-unreach-call.i

@@ -65,5 +65,5 @@ int main()
         }
     }
 END:
-    return;
+    return 0;
 }