Return value removal: handle missing declarations more gracefully

If a function is used before it is defined, a signature of int f(void)
is assumed. Then trying to use the (possibly non-existent) return value
fails during return-statement removal. In such cases, just assume a
non-deterministic value is being returned.

Found by running C-Reduce on a CSmith-generated example.

Author: tautschnig

regression/cbmc/return7/main.c

@@ -0,0 +1,17 @@
+void a()
+{
+  // Uses the implicit signature of undefined functions: int c(void)
+  int b = c();
+  __CPROVER_assert(b == 0, "expected to fail");
+}
+void c(void)
+{
+  // Actually... don't return anything
+  // So the results will be non-deterministic
+}
+
+int main(int argc, char **argv)
+{
+  a();
+  return 0;
+}

regression/cbmc/return7/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+Reason: Check return value
+^warning: ignoring

src/goto-programs/remove_returns.cpp

@@ -174,10 +174,10 @@ bool remove_returnst::do_function_calls(
         optionalt<symbol_exprt> return_value;
 
         if(!is_stub)
-        {
           return_value = get_or_create_return_value_symbol(function_id);
-          CHECK_RETURN(return_value.has_value());
 
+        if(return_value.has_value())
+        {
           // The return type in the definition of the function may differ
           // from the return type in the declaration.  We therefore do a
           // cast.
@@ -198,7 +198,7 @@ bool remove_returnst::do_function_calls(
         // fry the previous assignment
         function_call.lhs().make_nil();
 
-        if(!is_stub)
+        if(return_value.has_value())
         {
           goto_program.insert_after(
             t_a,