@@ -8,6 +8,7 @@ Author: Diffblue Ltd.
88
99#include " recursive_initialization.h"
1010
11+ #include < goto-programs/name_mangler.h>
1112#include < util/allocate_objects.h>
1213#include < util/arith_tools.h>
1314#include < util/c_types.h>
@@ -1008,6 +1009,27 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
10081009 for (const auto &target : targets)
10091010 {
10101011 auto const assign = code_assignt{dereference_exprt{result}, target};
1012+ auto const sym_to_lookup =
1013+ target.id () == ID_address_of
1014+ ?
1015+ // This is either address of or pointer; in pointer case, we don't
1016+ // need to do anything. In the address of case, the operand is
1017+ // a symbol representing a target function.
1018+ to_symbol_expr (to_address_of_expr (target).object ()).get_identifier ()
1019+ : " " ;
1020+ // skip referencing globals because the corresponding symbols in the symbol
1021+ // table are no longer marked as file local.
1022+ if (has_prefix (id2string (sym_to_lookup), FILE_LOCAL_PREFIX))
1023+ {
1024+ continue ;
1025+ }
1026+ else if (
1027+ goto_model.get_symbol_table ().lookup (sym_to_lookup) &&
1028+ goto_model.get_symbol_table ().lookup (sym_to_lookup)->is_file_local )
1029+ {
1030+ continue ;
1031+ }
1032+
10111033 if (function_pointer_index != targets.size () - 1 )
10121034 {
10131035 auto const condition = equal_exprt{
0 commit comments