Add tests for issue 3009 (#3526)

Kani v0.55 no longer has the overly broad span issue reported in #3009.
I suspect that our shift (#3363) from functions to closures for
contracts allows rustc to produce better error messages. Add tests to
prevent regression in the future.

Resolves #3009 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

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`

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
+}