From 7c35a479e535972a52c381a9430824d5ec2b3e6d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 12:24:18 -0600 Subject: [PATCH 1/9] Enable contracts for const generic functions --- .../src/sysroot/contracts/check.rs | 4 +-- .../src/sysroot/contracts/replace.rs | 20 ++++++++++++++ .../const_generic_function.expected | 1 + .../const_generic_function.rs | 27 +++++++++++++++++++ 4 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 tests/expected/function-contract/const_generic_function.expected create mode 100644 tests/expected/function-contract/const_generic_function.rs diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 863cf882f063..55a2062a8b40 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/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 diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index b28e178bea6d..9cd0e9b2a829 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -70,6 +70,8 @@ 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 +80,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 +101,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 +116,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 }) } diff --git a/tests/expected/function-contract/const_generic_function.expected b/tests/expected/function-contract/const_generic_function.expected new file mode 100644 index 000000000000..751e8bbb643e --- /dev/null +++ b/tests/expected/function-contract/const_generic_function.expected @@ -0,0 +1 @@ +Failed Checks: Check that *dst is assignable diff --git a/tests/expected/function-contract/const_generic_function.rs b/tests/expected/function-contract/const_generic_function.rs new file mode 100644 index 000000000000..c42271ae17e3 --- /dev/null +++ b/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. +//! + +struct Foo { + ptr: *const T, +} + +impl Foo { + #[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 = Foo { ptr: &x }; + unsafe { foo.bar(kani::any::()) }; +} From e73e32742dab713f4fc4a84a4bc5d41be596ddc8 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 12:31:23 -0600 Subject: [PATCH 2/9] Fix format --- library/kani_macros/src/sysroot/contracts/replace.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 9cd0e9b2a829..b41674395559 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -70,7 +70,6 @@ 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 } => { @@ -101,7 +100,7 @@ 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 From 2a27c9ebbfd63533bdf4003c3d653318786c362c Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 12:54:33 -0600 Subject: [PATCH 3/9] Fix typo --- library/kani_macros/src/sysroot/contracts/replace.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index b41674395559..da98385b3f15 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -119,7 +119,7 @@ impl<'a> ContractConditionsHandler<'a> { // 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 + #arg_redefinitions } #result }) From 922574a15ad37f8550ad67db9cee02c71058fbdc Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 15:12:25 -0600 Subject: [PATCH 4/9] Add redef only for contrats check mode --- .../src/sysroot/contracts/check.rs | 11 +++--- .../src/sysroot/contracts/replace.rs | 38 +++++++++---------- .../const_generic_function.expected | 1 + 3 files changed, 25 insertions(+), 25 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 55a2062a8b40..31851358cd95 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -84,7 +84,7 @@ impl<'a> ContractConditionsHandler<'a> { let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); let mut_recv = self.has_mutable_receiver().then(|| quote!(core::ptr::addr_of!(self),)); - let redefs = self.arg_redefinitions(); + let redefs = self.arg_redefinitions(true); let modifies_closure = self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); @@ -175,14 +175,13 @@ 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. - pub fn arg_redefinitions(&self) -> TokenStream2 { + pub fn arg_redefinitions(&self, redefine_only_mut: bool) -> 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 mut #ident = #ident;)); + } else if !redefine_only_mut { + result.extend(quote!(let #ident = #ident;)); } } result diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index da98385b3f15..1f140d114b42 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -70,7 +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(); + let redefs = self.arg_redefinitions(false); match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; @@ -79,12 +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 - } + + // 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 + #redefs + #result }) } @@ -100,12 +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 - } + + // 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 + #redefs + #result }) } @@ -115,12 +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 - } + + // 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 + #redefs + #result }) } diff --git a/tests/expected/function-contract/const_generic_function.expected b/tests/expected/function-contract/const_generic_function.expected index 751e8bbb643e..1303fcc8c426 100644 --- a/tests/expected/function-contract/const_generic_function.expected +++ b/tests/expected/function-contract/const_generic_function.expected @@ -1 +1,2 @@ + ** 1 of 83 failed Failed Checks: Check that *dst is assignable From 7687a4acd50b7f835f0b597abf8de5ceb1bac300 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 15:16:52 -0600 Subject: [PATCH 5/9] Fix format --- library/kani_macros/src/sysroot/contracts/replace.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 1f140d114b42..7927148262a8 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -84,7 +84,7 @@ impl<'a> ContractConditionsHandler<'a> { // to avoid may drop checks in const generic functions. // https://github.com/model-checking/kani/issues/3667 #redefs - + #result }) } From cae4a12e45c020cebcd44690592619a81d6b7265 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 15:41:24 -0600 Subject: [PATCH 6/9] Fix test --- .../expected/function-contract/const_generic_function.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/function-contract/const_generic_function.expected b/tests/expected/function-contract/const_generic_function.expected index 1303fcc8c426..c44061e214f6 100644 --- a/tests/expected/function-contract/const_generic_function.expected +++ b/tests/expected/function-contract/const_generic_function.expected @@ -1,2 +1,2 @@ - ** 1 of 83 failed + ** 1 of Failed Checks: Check that *dst is assignable From 0f7351e72c85358d8e22fbb419ddc858993ea9eb Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 18:54:12 -0600 Subject: [PATCH 7/9] Generate redefs only once --- .../kani_macros/src/sysroot/contracts/bootstrap.rs | 2 ++ library/kani_macros/src/sysroot/contracts/check.rs | 14 +++++++++----- .../src/sysroot/contracts/initialize.rs | 1 + library/kani_macros/src/sysroot/contracts/mod.rs | 2 ++ .../kani_macros/src/sysroot/contracts/replace.rs | 2 +- 5 files changed, 15 insertions(+), 6 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 5a9e12a62ae2..e9d54f41112d 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -21,6 +21,8 @@ impl<'a> ContractConditionsHandler<'a> { let recursion_name = &self.recursion_name; let check_name = &self.check_name; + // redefs will be used in replace_closure. + self.redefs = self.arg_redefinitions(false); let replace_closure = self.replace_closure(); let check_closure = self.check_closure(); let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure); diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 31851358cd95..a23efa034987 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -84,9 +84,12 @@ impl<'a> ContractConditionsHandler<'a> { let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); let mut_recv = self.has_mutable_receiver().then(|| quote!(core::ptr::addr_of!(self),)); - let redefs = self.arg_redefinitions(true); - let modifies_closure = - self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs); + let redefs_mut_only = self.arg_redefinitions(true); + let modifies_closure = self.modifies_closure( + &self.annotated_fn.sig.output, + &self.annotated_fn.block, + redefs_mut_only + ); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); parse_quote!( let #wrapper_arg_ident = (#mut_recv); @@ -172,9 +175,10 @@ impl<'a> ContractConditionsHandler<'a> { .unwrap_or(false) } - /// Generate argument re-definitions for mutable arguments. + /// Generate argument re-definitions for arguments. /// - /// This is used so Kani doesn't think that modifying a local argument value is a side effect. + /// This is used so Kani doesn't think that modifying a local argument value is a side effect, + /// and avoid may-drop checks in const generic functions. pub fn arg_redefinitions(&self, redefine_only_mut: bool) -> TokenStream2 { let mut result = TokenStream2::new(); for (mutability, ident) in self.arg_bindings() { diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index bd06139b27f5..482c30f0a9fa 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -80,6 +80,7 @@ impl<'a> ContractConditionsHandler<'a> { condition_type, annotated_fn, attr_copy, + redefs: Default::default(), output, check_name, replace_name, diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 41be536ffb6d..cc6156bf2131 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -475,6 +475,8 @@ struct ContractConditionsHandler<'a> { annotated_fn: &'a ItemFn, /// An unparsed, unmodified copy of `attr`, used in the error messages. attr_copy: TokenStream2, + /// Argument redefinitions. + redefs: TokenStream2, /// The stream to which we should write the generated code. output: TokenStream2, /// The name of the check closure. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 7927148262a8..8c0018ece7ad 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -70,7 +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 redefs = self.arg_redefinitions(false); + let redefs = &self.redefs; match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; From 579151659252603b894e0af8ba55878cd4cd1947 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 18 Nov 2024 18:59:24 -0600 Subject: [PATCH 8/9] Fix format --- library/kani_macros/src/sysroot/contracts/check.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index a23efa034987..6dbee0fd6c37 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -88,7 +88,7 @@ impl<'a> ContractConditionsHandler<'a> { let modifies_closure = self.modifies_closure( &self.annotated_fn.sig.output, &self.annotated_fn.block, - redefs_mut_only + redefs_mut_only, ); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); parse_quote!( From 3daad1f1c33b9130667d934ffc9666d8fc3b761f Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 19 Nov 2024 00:14:10 -0600 Subject: [PATCH 9/9] Move redefs to initialization of replace closure --- .../src/sysroot/contracts/bootstrap.rs | 2 -- .../src/sysroot/contracts/initialize.rs | 1 - .../kani_macros/src/sysroot/contracts/mod.rs | 2 -- .../src/sysroot/contracts/replace.rs | 34 +++++++------------ 4 files changed, 13 insertions(+), 26 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index e9d54f41112d..5a9e12a62ae2 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -21,8 +21,6 @@ impl<'a> ContractConditionsHandler<'a> { let recursion_name = &self.recursion_name; let check_name = &self.check_name; - // redefs will be used in replace_closure. - self.redefs = self.arg_redefinitions(false); let replace_closure = self.replace_closure(); let check_closure = self.check_closure(); let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure); diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index 482c30f0a9fa..bd06139b27f5 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -80,7 +80,6 @@ impl<'a> ContractConditionsHandler<'a> { condition_type, annotated_fn, attr_copy, - redefs: Default::default(), output, check_name, replace_name, diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index cc6156bf2131..41be536ffb6d 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -475,8 +475,6 @@ struct ContractConditionsHandler<'a> { annotated_fn: &'a ItemFn, /// An unparsed, unmodified copy of `attr`, used in the error messages. attr_copy: TokenStream2, - /// Argument redefinitions. - redefs: TokenStream2, /// The stream to which we should write the generated code. output: TokenStream2, /// The name of the check closure. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 8c0018ece7ad..b41985dea4c2 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -6,7 +6,7 @@ use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; use std::mem; -use syn::Stmt; +use syn::{Block, Stmt}; use super::{ ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, @@ -19,7 +19,18 @@ impl<'a> ContractConditionsHandler<'a> { fn initial_replace_stmts(&self) -> Vec { let return_type = return_type_to_type(&self.annotated_fn.sig.output); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)] + // 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 + let redefs = self.arg_redefinitions(false); + let redefs_block: Block = syn::parse_quote!({#redefs}); + vec![ + vec![syn::parse_quote!( + let #result : #return_type = kani::any_modifies(); + )], + redefs_block.stmts, + ] + .concat() } /// Split an existing replace body of the form @@ -70,7 +81,6 @@ 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 redefs = &self.redefs; match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; @@ -79,12 +89,6 @@ 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 - #redefs - #result }) } @@ -100,12 +104,6 @@ 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 - #redefs - #result }) } @@ -115,12 +113,6 @@ 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 - #redefs - #result }) }