Merge branch 'main' into toolchain-upgrade-3303

library/kani/src/internal.rs

@@ -90,3 +90,10 @@ pub fn untracked_deref<T>(_: &T) -> T {
 #[doc(hidden)]
 #[rustc_diagnostic_item = "KaniInitContracts"]
 pub fn init_contracts() {}
+
+/// This should only be used within contracts. The intent is to
+/// perform type inference on a closure's argument
+#[doc(hidden)]
+pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
+    f(x)
+}

library/kani_macros/src/sysroot/contracts/shared.rs

@@ -176,7 +176,7 @@ pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) {
         .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect));
 
     let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-    (remembers_stmts, Expr::Verbatim(quote!((#expr)(&#result))))
+    (remembers_stmts, Expr::Verbatim(quote!(kani::internal::apply_closure(#expr, &#result))))
 }
 
 trait OldTrigger {

tests/expected/function-contract/simple_ensures_pass_no_annotation.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|result| (*result == x) | (*result == y)"\
+in function max
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/simple_ensures_pass_no_annotation.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|result| (*result == x) | (*result == y))]
+fn max(x: u32, y: u32) -> u32 {
+    if x > y { x } else { y }
+}
+
+#[kani::proof_for_contract(max)]
+fn max_harness() {
+    let _ = Box::new(9_usize);
+    max(7, 6);
+}

tests/ui/function-contracts/mutating_ensures_error.expected

@@ -0,0 +1 @@
+cannot assign to `*_x`, as `Fn` closures cannot mutate their captured variables

tests/ui/function-contracts/mutating_ensures_error.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|_| {*_x += 1; true})]
+fn unit(_x: &mut u32) {}
+
+#[kani::proof_for_contract(id)]
+fn harness() {
+    let mut x = kani::any();
+    unit(&mut x);
+}