Skip to content

Commit c12ff79

Browse files
committed
Symex phi function: merge global variables like any other
Now that the front-ends are required to explicitly assign a nondet value where that is intended (e.g. an undefined extern global), rather than leaving an undefined value, there is no need to special-case merging them.
1 parent 3d46af3 commit c12ff79

File tree

1 file changed

+2
-6
lines changed

1 file changed

+2
-6
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -520,14 +520,10 @@ static void merge_names(
520520
rhs = goto_state_rhs;
521521
else if(goto_state.guard.is_false())
522522
rhs = dest_state_rhs;
523-
else if(goto_count == 0 && !symbol.is_static_lifetime)
524-
{
523+
else if(goto_count == 0)
525524
rhs = dest_state_rhs;
526-
}
527-
else if(dest_count == 0 && !symbol.is_static_lifetime)
528-
{
525+
else if(dest_count == 0)
529526
rhs = goto_state_rhs;
530-
}
531527
else
532528
{
533529
rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);

0 commit comments

Comments
 (0)