From e0141cf09819e90752dca6bf4d1b3cbb59997f17 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 2 Aug 2024 00:05:20 +0200
Subject: [PATCH] Remove unwind attributes that are no longer needed with CBMC
 v6 (#3403)

CBMC v6 includes https://github.com/diffblue/cbmc/pull/8247, which fixes
the need for unwind attributes that were newly found to be necessary
when upgrading to nightly-2024-03-15 (#3084).

Resolves: #3088
---
 docs/src/getting-started/verification-results/src/main.rs | 1 -
 tests/coverage/unreachable/abort/main.rs                  | 2 +-
 tests/expected/abort/main.rs                              | 1 -
 tests/expected/iterator/main.rs                           | 1 -
 tests/kani/Coroutines/main.rs                             | 1 -
 5 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/docs/src/getting-started/verification-results/src/main.rs b/docs/src/getting-started/verification-results/src/main.rs
index 72653cf4dc8f..7a03b34f0f9e 100644
--- a/docs/src/getting-started/verification-results/src/main.rs
+++ b/docs/src/getting-started/verification-results/src/main.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
-#[kani::unwind(4)]
 // ANCHOR: success_example
 fn success_example() {
     let mut sum = 0;
diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs
index 39c0b0efb54f..2941ec126f3c 100644
--- a/tests/coverage/unreachable/abort/main.rs
+++ b/tests/coverage/unreachable/abort/main.rs
@@ -5,7 +5,7 @@
 
 use std::process;
 
-#[cfg_attr(kani, kani::proof, kani::unwind(5))]
+#[kani::proof]
 fn main() {
     for i in 0..4 {
         if i == 1 {
diff --git a/tests/expected/abort/main.rs b/tests/expected/abort/main.rs
index 9e2f5b7a808c..2941ec126f3c 100644
--- a/tests/expected/abort/main.rs
+++ b/tests/expected/abort/main.rs
@@ -6,7 +6,6 @@
 use std::process;
 
 #[kani::proof]
-#[kani::unwind(5)]
 fn main() {
     for i in 0..4 {
         if i == 1 {
diff --git a/tests/expected/iterator/main.rs b/tests/expected/iterator/main.rs
index 5cf9402bcb23..b1cb4a89cfbf 100644
--- a/tests/expected/iterator/main.rs
+++ b/tests/expected/iterator/main.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
-#[kani::unwind(4)]
 fn main() {
     let mut z = 1;
     for i in 1..4 {
diff --git a/tests/kani/Coroutines/main.rs b/tests/kani/Coroutines/main.rs
index e059305a6da2..0742d14a6ada 100644
--- a/tests/kani/Coroutines/main.rs
+++ b/tests/kani/Coroutines/main.rs
@@ -10,7 +10,6 @@ use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
-#[kani::unwind(3)]
 fn main() {
     let mut add_one = #[coroutine]
     |mut resume: u8| {