Skip to content

Commit d7bb937

Browse files
martinmartin
martin
authored and
martin
committed
Catch the case when a GOTO instruction is effectively a SKIP.
This is rare in usual work-flows as remove_skip should remove this. However if the program has been extensively transformed it could happen.
1 parent b2fba97 commit d7bb937

File tree

1 file changed

+7
-4
lines changed

1 file changed

+7
-4
lines changed

src/analyses/interval_domain.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -82,10 +82,13 @@ void interval_domaint::transform(
8282
// of instructions because this is a GOTO.
8383
locationt next=from;
8484
next++;
85-
if(next==to)
86-
assume(not_exprt(instruction.guard), ns);
87-
else
88-
assume(instruction.guard, ns);
85+
if(from->get_target() != next) // If equal then a skip
86+
{
87+
if(next == to)
88+
assume(not_exprt(instruction.guard), ns);
89+
else
90+
assume(instruction.guard, ns);
91+
}
8992
}
9093
break;
9194

0 commit comments

Comments
 (0)