diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 854a706e5e7..419c6d2f3ba 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -233,17 +233,18 @@ void remove_function_pointerst::fix_return_type( code_type.return_type(), ns)) return; + const symbolt &function_symbol = + ns.lookup(to_symbol_expr(function_call.function()).get_identifier()); + symbolt &tmp_symbol = get_fresh_aux_symbol( code_type.return_type(), id2string(function_call.source_location().get_function()), - "tmp_return_val", + "tmp_return_val_" + id2string(function_symbol.base_name), function_call.source_location(), - irep_idt(), + function_symbol.mode, symbol_table); - symbol_exprt tmp_symbol_expr; - tmp_symbol_expr.type()=tmp_symbol.type; - tmp_symbol_expr.set_identifier(tmp_symbol.name); + const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr(); exprt old_lhs=function_call.lhs(); function_call.lhs()=tmp_symbol_expr;