remove_returns: ensure type consistency of return value assignment

Author: Daniel Kroening

regression/cbmc/Linking7/return_type.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 return_type1.c
 return_type2.c
 ^EXIT=0$

src/goto-programs/remove_returns.cpp

@@ -189,7 +189,13 @@ void remove_returnst::do_function_calls(
           exprt rhs;
 
           if(!is_stub)
-            rhs=return_value;
+          {
+            // The return type in the definition of the function may differ
+            // from the return type in the declaration.  We therefore do a
+            // cast.
+            rhs = typecast_exprt::conditional_cast(
+              return_value, function_call.lhs().type());
+          }
           else
             rhs = side_effect_expr_nondett(
               function_call.lhs().type(), i_it->source_location);
@@ -208,7 +214,7 @@ void remove_returnst::do_function_calls(
             goto_programt::targett t_d=goto_program.insert_after(t_a);
             t_d->make_dead();
             t_d->source_location=i_it->source_location;
-            t_d->code=code_deadt(rhs);
+            t_d->code = code_deadt(return_value);
             t_d->function=i_it->function;
           }
         }