Skip to content

Commit eca9b59

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 eca9b59

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -476,15 +476,17 @@ 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 only apply to dynamic objects and locals.
479481
if(dest_state.guard.is_false())
480482
rhs = goto_state_rhs;
481483
else if(goto_state.guard.is_false())
482484
rhs = dest_state_rhs;
483-
else if(goto_count == 0 && symbol.value.is_not_nil())
485+
else if(goto_count == 0 && !symbol.is_static_lifetime)
484486
{
485487
rhs = dest_state_rhs;
486488
}
487-
else if(dest_count == 0 && symbol.value.is_not_nil())
489+
else if(dest_count == 0 && !symbol.is_static_lifetime)
488490
{
489491
rhs = goto_state_rhs;
490492
}

0 commit comments

Comments
 (0)