Skip to content

Commit

Permalink
Catch the case when a GOTO instruction is effectively a SKIP.
Browse files Browse the repository at this point in the history
This is rare in usual work-flows as remove_skip should remove this.
However if the program has been extensively transformed it could
happen.
  • Loading branch information
martin authored and martin committed Feb 9, 2018
1 parent b2fba97 commit d7bb937
Showing 1 changed file with 7 additions and 4 deletions.
11 changes: 7 additions & 4 deletions src/analyses/interval_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -82,10 +82,13 @@ void interval_domaint::transform(
// of instructions because this is a GOTO.
locationt next=from;
next++;
if(next==to)
assume(not_exprt(instruction.guard), ns);
else
assume(instruction.guard, ns);
if(from->get_target() != next) // If equal then a skip
{
if(next == to)
assume(not_exprt(instruction.guard), ns);
else
assume(instruction.guard, ns);
}
}
break;

Expand Down

0 comments on commit d7bb937

Please sign in to comment.