Replace a missing return value by nondet

tautschnig · tautschnig · commit 7872f7cb33d1 · 2018-04-16T13:02:18.000+01:00
A missing return value is undefined behaviour. Previously the code would return
0, which is unsound, and wouldn't even yield a warning.
diff --git a/regression/cbmc/return2/main.c b/regression/cbmc/return2/main.c
@@ -0,0 +1,23 @@
+int missing_return(int x)
+{
+  if(x)
+    return x;
+
+  // missing return statement
+}
+
+int missing_return_value(int x)
+{
+  if(x)
+    return x;
+
+  return; // missing value
+}
+
+int main()
+{
+  __CPROVER_assert(missing_return(0) == 0, "expected to fail");
+  __CPROVER_assert(missing_return_value(0) == 0, "expected to fail");
+
+  return 0;
+}
diff --git a/regression/cbmc/return2/test.desc b/regression/cbmc/return2/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion..\] expected to fail: FAILURE$
+\*\* 2 of 2 failed
+--
+^warning: ignoring
+\[main.assertion..\] expected to fail: SUCCESS$
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_typecheck_base.h"
 
 #include <util/config.h>
-#include <linking/zero_initializer.h>
 
 #include "ansi_c_declaration.h"
 
@@ -670,11 +669,10 @@ void c_typecheck_baset::typecheck_return(codet &code)
        return_type.id()!=ID_destructor)
     {
       // gcc doesn't actually complain, it just warns!
-      // We'll put a zero here, which is dubious.
-      exprt zero=
-        zero_initializer(
-          return_type, code.source_location(), *this, get_message_handler());
-      code.copy_to_operands(zero);
+      warning().source_location = code.source_location();
+      warning() << "non-void function should return a value" << eom;
+
+      code.copy_to_operands(side_effect_expr_nondett(return_type));
     }
   }
   else if(code.operands().size()==1)
