File tree 1 file changed +6
-5
lines changed
1 file changed +6
-5
lines changed Original file line number Diff line number Diff line change @@ -233,17 +233,18 @@ void remove_function_pointerst::fix_return_type(
233
233
code_type.return_type (), ns))
234
234
return ;
235
235
236
+ const symbolt &function_symbol =
237
+ ns.lookup (to_symbol_expr (function_call.function ()).get_identifier ());
238
+
236
239
symbolt &tmp_symbol = get_fresh_aux_symbol (
237
240
code_type.return_type (),
238
241
id2string (function_call.source_location ().get_function ()),
239
- " tmp_return_val " ,
242
+ " tmp_return_val_ " + id2string (function_symbol. base_name ) ,
240
243
function_call.source_location (),
241
- irep_idt () ,
244
+ function_symbol. mode ,
242
245
symbol_table);
243
246
244
- symbol_exprt tmp_symbol_expr;
245
- tmp_symbol_expr.type ()=tmp_symbol.type ;
246
- tmp_symbol_expr.set_identifier (tmp_symbol.name );
247
+ const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr ();
247
248
248
249
exprt old_lhs=function_call.lhs ();
249
250
function_call.lhs ()=tmp_symbol_expr;
You can’t perform that action at this time.
0 commit comments