Remove kani::Arbitrary from the modifies contract instrumentation

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

@@ -60,7 +60,8 @@ impl<'a> ContractConditionsHandler<'a> {
                 let wrapper_args = if let Some(wrapper_call_args) =
                     inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name))
                 {
-                    let wrapper_args = make_wrapper_args(wrapper_call_args.len(), attr.len());
+                    let wrapper_args =
+                        make_wrapper_idents(wrapper_call_args.len(), attr.len(), "_wrapper_arg_");
                     wrapper_call_args
                         .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a))));
                     wrapper_args
@@ -129,15 +130,34 @@ impl<'a> ContractConditionsHandler<'a> {
     /// each expression in the clause.
     pub fn emit_augmented_modifies_wrapper(&mut self) {
         if let ContractConditionsData::Modifies { attr } = &self.condition_type {
-            let wrapper_args = make_wrapper_args(self.annotated_fn.sig.inputs.len(), attr.len());
+            let wrapper_args = make_wrapper_idents(
+                self.annotated_fn.sig.inputs.len(),
+                attr.len(),
+                "_wrapper_arg_",
+            );
+            // Generate a unique type parameter identifier
+            let type_params = make_wrapper_idents(
+                self.annotated_fn.sig.inputs.len(),
+                attr.len(),
+                "WrapperArgType",
+            );
             let sig = &mut self.annotated_fn.sig;
-            for arg in wrapper_args.clone() {
+            for (arg, arg_type) in wrapper_args.clone().zip(type_params) {
+                // Add the type parameter to the function signature's generic parameters list
+                sig.generics.params.push(syn::GenericParam::Type(syn::TypeParam {
+                    attrs: vec![],
+                    ident: arg_type.clone(),
+                    colon_token: None,
+                    bounds: Default::default(),
+                    eq_token: None,
+                    default: None,
+                }));
                 let lifetime = syn::Lifetime { apostrophe: Span::call_site(), ident: arg.clone() };
                 sig.inputs.push(FnArg::Typed(syn::PatType {
                     attrs: vec![],
                     colon_token: Token![:](Span::call_site()),
                     pat: Box::new(syn::Pat::Verbatim(quote!(#arg))),
-                    ty: Box::new(syn::Type::Verbatim(quote!(&#lifetime impl kani::Arbitrary))),
+                    ty: Box::new(syn::parse_quote! { &#arg_type }),
                 }));
                 sig.generics.params.push(syn::GenericParam::Lifetime(syn::LifetimeParam {
                     lifetime,
@@ -146,6 +166,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     attrs: vec![],
                 }));
             }
+
             self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)]))
         }
         self.emit_common_header();
@@ -193,8 +214,12 @@ fn try_as_wrapper_call_args<'a>(
 
 /// Make `num` [`Ident`]s with the names `_wrapper_arg_{i}` with `i` starting at `low` and
 /// increasing by one each time.
-fn make_wrapper_args(low: usize, num: usize) -> impl Iterator<Item = syn::Ident> + Clone {
-    (low..).map(|i| Ident::new(&format!("_wrapper_arg_{i}"), Span::mixed_site())).take(num)
+fn make_wrapper_idents(
+    low: usize,
+    num: usize,
+    prefix: &'static str,
+) -> impl Iterator<Item = syn::Ident> + Clone + 'static {
+    (low..).map(move |i| Ident::new(&format!("{}{}", prefix, i), Span::mixed_site())).take(num)
 }
 
 #[cfg(test)]