Skip to content

Commit 6009066

Browse files
committed
Contracts/insert_before_and_update_jumps: only update jump edge
The incoming edge from a `goto` instruction may also be the non-branching case, which must not result in redirecting this goto.
1 parent 2bc9b22 commit 6009066

File tree

3 files changed

+3
-3
lines changed

3 files changed

+3
-3
lines changed

regression/contracts-dfcc/loop_contracts_do_while/assigns.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE dfcc-only
22
assigns.c
33
--dfcc main --apply-loop-contracts
44
^EXIT=0$

regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE dfcc-only
22
side_effect.c
33
--dfcc main --apply-loop-contracts
44
^EXIT=0$

src/goto-instrument/contracts/utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -250,7 +250,7 @@ void insert_before_and_update_jumps(
250250
const auto new_target = destination.insert_before(target, i);
251251
for(auto it : target->incoming_edges)
252252
{
253-
if(it->is_goto())
253+
if(it->is_goto() && it->get_target() == target)
254254
it->set_target(new_target);
255255
}
256256
}

0 commit comments

Comments
 (0)