Skip to content

Commit 3b3dc71

Browse files
committed
Distinct names of return-value symbols
Function-pointer removal spends 43.52% of its time in get_max when working on the Linux kernel. By avoiding repeated use of the same prefix for all calls that a function pointer may expand to, the number of calls to get_max is reduced, resulting in a total runtime reduction from 1457s to 640s.
1 parent 4f7fade commit 3b3dc71

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/goto-programs/remove_function_pointers.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -239,7 +239,7 @@ void remove_function_pointerst::fix_return_type(
239239
symbolt &tmp_symbol = get_fresh_aux_symbol(
240240
code_type.return_type(),
241241
id2string(function_call.source_location().get_function()),
242-
"tmp_return_val",
242+
"tmp_return_val_" + id2string(function_symbol.base_name),
243243
function_call.source_location(),
244244
function_symbol.mode,
245245
symbol_table);

0 commit comments

Comments
 (0)