Skip to content

Commit e4b8549

Browse files
committed
Narrowing the scope of the global extern phi merge check
The is_not_nil check was a little broad and causing uninitialized values to get merged in some situations. Made the condition for being an external global stricter.
1 parent 9f632e2 commit e4b8549

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -476,15 +476,21 @@ static void merge_names(
476476
// 1. Either guard is false, so we can't follow that branch.
477477
// 2. Either identifier is of generation zero, and so hasn't been
478478
// initialized and therefore an invalid target.
479+
480+
// These rules don't apply to global externs, which can be uninitialized and
481+
// are still valid targets.
482+
bool is_global_extern =
483+
symbol.is_extern && symbol.is_static_lifetime && !symbol.value.is_not_nil();
484+
479485
if(dest_state.guard.is_false())
480486
rhs = goto_state_rhs;
481487
else if(goto_state.guard.is_false())
482488
rhs = dest_state_rhs;
483-
else if(goto_count == 0 && symbol.value.is_not_nil())
489+
else if(goto_count == 0 && !is_global_extern)
484490
{
485491
rhs = dest_state_rhs;
486492
}
487-
else if(dest_count == 0 && symbol.value.is_not_nil())
493+
else if(dest_count == 0 && !is_global_extern)
488494
{
489495
rhs = goto_state_rhs;
490496
}

0 commit comments

Comments
 (0)