From 7872f7cb33d14a1e5f909e961e11eaf37abf32d5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 2 Mar 2018 17:24:21 +0000
Subject: [PATCH] Replace a missing return value by nondet

A missing return value is undefined behaviour. Previously the code would return
0, which is unsound, and wouldn't even yield a warning.
---
 regression/cbmc/return2/main.c    | 23 +++++++++++++++++++++++
 regression/cbmc/return2/test.desc | 11 +++++++++++
 src/ansi-c/c_typecheck_code.cpp   | 10 ++++------
 3 files changed, 38 insertions(+), 6 deletions(-)
 create mode 100644 regression/cbmc/return2/main.c
 create mode 100644 regression/cbmc/return2/test.desc

diff --git a/regression/cbmc/return2/main.c b/regression/cbmc/return2/main.c
new file mode 100644
index 00000000000..a79f3d56785
--- /dev/null
+++ 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
new file mode 100644
index 00000000000..d383de8d1c9
--- /dev/null
+++ 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
index 5529ab6213b..c025aa1fb6b 100644
--- 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)