From 042eb473d62305820f0db315d139ca152cb608b2 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 18 Sep 2024 15:29:04 -0400
Subject: [PATCH] add tests for issue 3009

---
 .../function-contracts/non_bool_contracts.expected  | 11 +++++++++++
 tests/ui/function-contracts/non_bool_contracts.rs   | 13 +++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 tests/ui/function-contracts/non_bool_contracts.expected
 create mode 100644 tests/ui/function-contracts/non_bool_contracts.rs

diff --git a/tests/ui/function-contracts/non_bool_contracts.expected b/tests/ui/function-contracts/non_bool_contracts.expected
new file mode 100644
index 000000000000..a6d7704330db
--- /dev/null
+++ b/tests/ui/function-contracts/non_bool_contracts.expected
@@ -0,0 +1,11 @@
+|
+| #[kani::requires(a + b)]
+| -----------------^^^^^--
+| |                |
+| |                expected `bool`, found `u64`
+| arguments to this function are incorrect
+|
+
+|
+| #[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)]
+|                          ^^^^^^^^^^^ expected `bool`, found `u64`
\ No newline at end of file
diff --git a/tests/ui/function-contracts/non_bool_contracts.rs b/tests/ui/function-contracts/non_bool_contracts.rs
new file mode 100644
index 000000000000..e192e625cac3
--- /dev/null
+++ b/tests/ui/function-contracts/non_bool_contracts.rs
@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// This tests that Kani reports the "ideal" error message when contracts are non-boolean expressions
+// By "ideal," we mean that the error spans are as narrow as possible
+// (c.f. https://github.com/model-checking/kani/issues/3009)
+
+#[kani::requires(a + b)]
+#[kani::ensures(|result| a % *result && b % *result == 0 && *result != 0)]
+fn gcd(a: u64, b: u64) -> u64 {
+    0
+}