Skip to content

Commit 8372862

Browse files
committed
function-pointer removal: Set the mode of a return symbol
1 parent f156ef0 commit 8372862

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/goto-programs/remove_function_pointers.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -233,12 +233,15 @@ void remove_function_pointerst::fix_return_type(
233233
code_type.return_type(), ns))
234234
return;
235235

236+
const symbolt &function_symbol =
237+
ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
238+
236239
symbolt &tmp_symbol = get_fresh_aux_symbol(
237240
code_type.return_type(),
238241
id2string(function_call.source_location().get_function()),
239242
"tmp_return_val",
240243
function_call.source_location(),
241-
irep_idt(),
244+
function_symbol.mode,
242245
symbol_table);
243246

244247
symbol_exprt tmp_symbol_expr;

0 commit comments

Comments
 (0)