From adc1f0df9728e39149996fad7f35068275619e88 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 8 Jun 2024 17:02:41 +0200
Subject: [PATCH] Do not turn trivially diverging loops into assume(false)
 (#3223)

CBMC's symbolic execution by default turns `while(true) {}` loops into
`assume(false)` to counter trivial non-termination of symbolic
execution. When unwinding assertions are enabled, however, we should
report the non-termination of such loops.

Resolves: #2909
---
 kani-driver/src/call_cbmc.rs                      |  2 ++
 .../function-contract/diverging_loop.expected     |  3 +++
 .../expected/function-contract/diverging_loop.rs  | 15 +++++++++++++++
 3 files changed, 20 insertions(+)
 create mode 100644 tests/expected/function-contract/diverging_loop.expected
 create mode 100644 tests/expected/function-contract/diverging_loop.rs

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 7d0edf6f50e5..7a623253f3a3 100644
--- 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
new file mode 100644
index 000000000000..05c2856a7c31
--- /dev/null
+++ 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
new file mode 100644
index 000000000000..219f723494f7
--- /dev/null
+++ 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();
+}