Skip to content

Commit

Permalink
Contracts/insert_before_and_update_jumps: only update jump edge
Browse files Browse the repository at this point in the history
The incoming edge from a `goto` instruction may also be the
non-branching case, which must not result in redirecting this goto.
  • Loading branch information
tautschnig committed Aug 20, 2024
1 parent 180d06f commit 60d7d4a
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
assigns.c
--dfcc main --apply-loop-contracts
^EXIT=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
side_effect.c
--dfcc main --apply-loop-contracts
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/contracts/utils.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ void insert_before_and_update_jumps(
const auto new_target = destination.insert_before(target, i);
for(auto it : target->incoming_edges)
{
if(it->is_goto())
if(it->is_goto() && it->get_target() == target)
it->set_target(new_target);
}
}
Expand Down

0 comments on commit 60d7d4a

Please sign in to comment.