Merge pull request #301 from thk123/void-return-warning

Added a warning for when function returns a value but has return void

Author: Daniel Kroening

regression/ansi-c/function_return1/main.c

@@ -0,0 +1,4 @@
+void fun()
+{
+  return 5;
+}

regression/ansi-c/function_return1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--verbosity 2
+^file main.c line 3 function fun: function has return void but a return statement returning signed int$
+^SIGNAL=0$
+
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_code.cpp

@@ -911,7 +911,16 @@ void c_typecheck_baset::typecheck_return(codet &code)
     {
       // gcc doesn't actually complain, it just warns!
       if(follow(code.op0().type()).id()!=ID_empty)
+      {
+        warning().source_location=code.source_location();
+
+        warning() << "function has return void ";
+        warning() << "but a return statement returning ";
+        warning() << to_string(follow(code.op0().type()));
+        warning() << eom;
+
         code.op0().make_typecast(return_type);
+      }
     }
     else
       implicit_typecast(code.op0(), return_type);