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,7 @@
+void a()
+{
+  int b = c();
+}
+void c(void)
+{
+}

regression/cbmc/return7/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+the program has no entry point
+^EXIT=6$
+^SIGNAL=0$
+--
+Reason: Check return value
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

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,