Remove unwind attributes that are no longer needed with CBMC v6 (mode…

…l-checking#3403) CBMC v6 includes diffblue/cbmc#8247, which fixes the need for unwind attributes that were newly found to be necessary when upgrading to nightly-2024-03-15 (model-checking#3084). Resolves: model-checking#3088
tautschnig · Aug 1, 2024 · e0141cf · e0141cf
1 parent d6d1ebf
commit e0141cf
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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| {