Enable contracts for const generic functions

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

@@ -175,14 +175,14 @@ impl<'a> ContractConditionsHandler<'a> {
     /// Generate argument re-definitions for mutable arguments.
     ///
     /// This is used so Kani doesn't think that modifying a local argument value is a side effect.
-    fn arg_redefinitions(&self) -> TokenStream2 {
+    pub fn arg_redefinitions(&self) -> TokenStream2 {
         let mut result = TokenStream2::new();
         for (mutability, ident) in self.arg_bindings() {
             if mutability == MutBinding::Mut {
                 result.extend(quote!(let mut #ident = #ident;))
             } else {
                 // This would make some replace some temporary variables from error messages.
-                //result.extend(quote!(let #ident = #ident; ))
+                result.extend(quote!(let #ident = #ident; ))
             }
         }
         result

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

@@ -70,6 +70,7 @@ impl<'a> ContractConditionsHandler<'a> {
     /// `use_nondet_result` will only be true if this is the first time we are
     /// generating a replace function.
     fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
+        let arg_redefinitions = self.arg_redefinitions();
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 let Self { attr_copy, .. } = self;
@@ -78,6 +79,12 @@ impl<'a> ContractConditionsHandler<'a> {
                     kani::assert(#attr, stringify!(#attr_copy));
                     #(#before)*
                     #(#after)*
+                    {
+                        // Add dummy assignments of the input variables to local variables
+                        // to avoid may drop checks in const generic functions.
+                        // https://github.com/model-checking/kani/issues/3667
+                        #arg_redefinitions
+                    }
                     #result
                 })
             }
@@ -93,6 +100,12 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#rest_of_before)*
                     #(#after)*
                     kani::assume(#ensures_clause);
+                    {
+                        // Add dummy assignments of the input variables to local variables
+                        // to avoid may drop checks in const generic functions.
+                        // https://github.com/model-checking/kani/issues/3667
+                        #arg_redefinitions
+                    }
                     #result
                 })
             }
@@ -102,6 +115,12 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#before)*
                     #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)*
                     #(#after)*
+                    {
+                        // Add dummy assignments of the input variables to local variables
+                        // to avoid may drop checks in const generic functions.
+                        // https://github.com/model-checking/kani/issues/3667
+                        #arg_redefinitions
+                    }
                     #result
                 })
             }

tests/expected/function-contract/const_generic_function.expected

@@ -0,0 +1 @@
+Failed Checks: Check that *dst is assignable

tests/expected/function-contract/const_generic_function.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check that Kani contract can be applied to a constant generic function.
+//! <https://github.com/model-checking/kani/issues/3667>
+
+struct Foo<T> {
+    ptr: *const T,
+}
+
+impl<T: Sized> Foo<T> {
+    #[kani::requires(true)]
+    pub const unsafe fn bar(self, v: T)
+    where
+        T: Sized,
+    {
+        unsafe { core::ptr::write(self.ptr as *mut T, v) };
+    }
+}
+
+#[kani::proof_for_contract(Foo::bar)]
+fn check_const_generic_function() {
+    let x: u8 = kani::any();
+    let foo: Foo<u8> = Foo { ptr: &x };
+    unsafe { foo.bar(kani::any::<u8>()) };
+}