Skip to content

Commit 3b2494f

Browse files
committed
Add fix for file local symbols referencing
1 parent a19f027 commit 3b2494f

File tree

1 file changed

+22
-0
lines changed

1 file changed

+22
-0
lines changed

src/goto-harness/recursive_initialization.cpp

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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

Comments
 (0)