diff --git a/regression/cbmc/Linking7/return_type.desc b/regression/cbmc/Linking7/return_type.desc new file mode 100644 index 00000000000..e51bc4611dd --- /dev/null +++ b/regression/cbmc/Linking7/return_type.desc @@ -0,0 +1,10 @@ +CORE +return_type1.c +return_type2.c +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Note issue #3081 diff --git a/regression/cbmc/Linking7/return_type1.c b/regression/cbmc/Linking7/return_type1.c new file mode 100644 index 00000000000..eb05a3e45c8 --- /dev/null +++ b/regression/cbmc/Linking7/return_type1.c @@ -0,0 +1,13 @@ +#include + +struct S +{ + int i; +}; + +struct S *function(); + +int main() +{ + assert(function() != 0); +} diff --git a/regression/cbmc/Linking7/return_type2.c b/regression/cbmc/Linking7/return_type2.c new file mode 100644 index 00000000000..598484e7095 --- /dev/null +++ b/regression/cbmc/Linking7/return_type2.c @@ -0,0 +1,10 @@ +struct S +{ + int i; + int j; // extra member +} some_var; + +struct S *function() +{ + return &some_var; +} diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 75c862c62f4..126b23a1ee3 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/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; } }