Function Contracts: Closure Type Inference

library/kani/src/lib.rs

@@ -326,3 +326,7 @@ pub use kani_macros::*;
 pub(crate) use kani_macros::unstable_feature as unstable;
 
 pub mod contracts;
+
+pub fn apply_closure<T, U: FnOnce(&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::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);
+}