Merge remote-tracking branch 'origin/main' into toolchain-2024-06-04-…

…manual
tautschnig · Jun 10, 2024 · c2f5632 · c2f5632
2 parents 7636ee3 + adc1f0d
commit c2f5632
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 0 deletions.
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -182,7 +182,9 @@ impl KaniSession {
  }
 
  if self.args.checks.unwinding_on() {
+ // TODO: With CBMC v6 the below can be removed as those are defaults.
  args.push("--unwinding-assertions".into());
+ args.push("--no-self-loops-to-assumptions".into());
  }
 
  if self.args.extra_pointer_checks {

diff --git a/tests/expected/function-contract/diverging_loop.expected b/tests/expected/function-contract/diverging_loop.expected
@@ -0,0 +1,3 @@
+Failed Checks: unwinding assertion loop 0
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/diverging_loop.rs b/tests/expected/function-contract/diverging_loop.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|result : &i32| *result == 1)]
+fn foo() -> i32 {
+ loop {}
+ 2
+}
+
+#[kani::proof_for_contract(foo)]
+#[kani::unwind(1)]
+fn check_foo() {
+ let _ = foo();
+}