From 88d20913598a2749e0ffe749c7f46b93e6ae7c04 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 07:18:38 +0000 Subject: [PATCH] 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. --- regression/contracts-dfcc/loop_contracts_do_while/assigns.desc | 2 +- .../contracts-dfcc/loop_contracts_do_while/side_effect.desc | 2 +- src/goto-instrument/contracts/utils.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc index 7149815c6d9..4fe2cf25dde 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/assigns.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE dfcc-only assigns.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc index 6f9b34dd89c..6306416f3bf 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc +++ b/regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE dfcc-only side_effect.c --dfcc main --apply-loop-contracts ^EXIT=0$ diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 803cf47eb6a..6dd6cf7e681 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -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); } }