diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 4f963038cab9..65b9ec7c01cc 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -51,14 +51,14 @@ //! approximation of the result of division for instance could be this: //! //! ``` -//! #[ensures(result <= dividend)] +//! #[ensures(|result : &u32| *result <= dividend)] //! ``` //! //! This is called a postcondition and it also has access to the arguments and //! is expressed in regular Rust code. The same restrictions apply as did for -//! [`requires`][macro@requires]. In addition to the arguments the postcondition -//! also has access to the value returned from the function in a variable called -//! `result`. +//! [`requires`][macro@requires]. In addition to the postcondition is expressed +//! as a closure where the value returned from the function is passed to this +//! closure by reference. //! //! You may combine as many [`requires`][macro@requires] and //! [`ensures`][macro@ensures] attributes on a single function as you please. @@ -67,7 +67,7 @@ //! //! ``` //! #[kani::requires(divisor != 0)] -//! #[kani::ensures(result <= dividend)] +//! #[kani::ensures(|result : &u32| *result <= dividend)] //! fn my_div(dividend: u32, divisor: u32) -> u32 { //! dividend / divisor //! } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 0991730f8802..44a0ca78ea41 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -131,11 +131,11 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// This is part of the function contract API, for more general information see /// the [module-level documentation](../kani/contracts/index.html). /// -/// The contents of the attribute is a condition over the input values to the -/// annotated function *and* its return value, accessible as a variable called -/// `result`. All Rust syntax is supported, even calling other functions, but -/// the computations must be side effect free, e.g. it cannot perform I/O or use -/// mutable memory. +/// The contents of the attribute is a closure that captures the input values to +/// the annotated function and the input to the function is the return value of +/// the function passed by reference. All Rust syntax is supported, even calling +/// other functions, but the computations must be side effect free, e.g. it +/// cannot perform I/O or use mutable memory. /// /// Kani requires each function that uses a contract (this attribute or /// [`requires`][macro@requires]) to have at least one designated diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 8d930fdebda9..7c35cc469254 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -4,11 +4,14 @@ //! Special way we handle the first time we encounter a contract attribute on a //! function. -use proc_macro2::Span; +use proc_macro2::{Ident, Span}; use quote::quote; use syn::ItemFn; -use super::{helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler}; +use super::{ + helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler, + INTERNAL_RESULT_IDENT, +}; impl<'a> ContractConditionsHandler<'a> { /// The complex case. We are the first time a contract is handled on this function, so @@ -80,6 +83,7 @@ impl<'a> ContractConditionsHandler<'a> { (quote!(#check_fn_name), quote!(#replace_fn_name)) }; + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); self.output.extend(quote!( #[allow(dead_code, unused_variables)] #[kanitool::is_contract_generated(recursion_wrapper)] @@ -89,9 +93,9 @@ impl<'a> ContractConditionsHandler<'a> { #call_replace(#(#args),*) } else { unsafe { REENTRY = true }; - let result = #call_check(#(#also_args),*); + let #result = #call_check(#(#also_args),*); unsafe { REENTRY = false }; - result + #result } } )); diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 516bd187ba7f..473535e8d8fd 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -10,7 +10,7 @@ use syn::{Expr, FnArg, ItemFn, Token}; use super::{ helpers::*, shared::{make_unsafe_argument_copies, try_as_result_assign_mut}, - ContractConditionsData, ContractConditionsHandler, + ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; const WRAPPER_ARG_PREFIX: &str = "_wrapper_arg_"; @@ -46,14 +46,15 @@ impl<'a> ContractConditionsHandler<'a> { assert!(matches!( inner.pop(), Some(syn::Stmt::Expr(syn::Expr::Path(pexpr), None)) - if pexpr.path.get_ident().map_or(false, |id| id == "result") + if pexpr.path.get_ident().map_or(false, |id| id == INTERNAL_RESULT_IDENT) )); + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #arg_copies #(#inner)* #exec_postconditions - result + #result ) } ContractConditionsData::Modifies { attr } => { @@ -95,9 +96,10 @@ impl<'a> ContractConditionsHandler<'a> { } else { quote!(#wrapper_name) }; + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); syn::parse_quote!( - let result : #return_type = #wrapper_call(#(#args),*); - result + let #result : #return_type = #wrapper_call(#(#args),*); + #result ) } else { self.annotated_fn.block.stmts.clone() diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index 6452ab9ace62..aee0c21bc82d 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -7,12 +7,13 @@ use std::collections::{HashMap, HashSet}; use proc_macro::{Diagnostic, TokenStream}; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; -use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ItemFn, Signature}; +use quote::quote; +use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn}; use super::{ helpers::{chunks_by, is_token_stream_2_comma, matches_path}, ContractConditionsData, ContractConditionsHandler, ContractConditionsType, - ContractFunctionState, + ContractFunctionState, INTERNAL_RESULT_IDENT, }; impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { @@ -81,7 +82,11 @@ impl<'a> ContractConditionsHandler<'a> { ContractConditionsData::Requires { attr: syn::parse(attr)? } } ContractConditionsType::Ensures => { - ContractConditionsData::new_ensures(&annotated_fn.sig, syn::parse(attr)?) + let mut data: ExprClosure = syn::parse(attr)?; + let argument_names = rename_argument_occurrences(&annotated_fn.sig, &mut data); + let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + let app: Expr = Expr::Verbatim(quote!((#data)(&#result))); + ContractConditionsData::Ensures { argument_names, attr: app } } ContractConditionsType::Modifies => { ContractConditionsData::new_modifies(attr, &mut output) @@ -92,16 +97,6 @@ impl<'a> ContractConditionsHandler<'a> { } } impl ContractConditionsData { - /// Constructs a [`Self::Ensures`] from the signature of the decorated - /// function and the contents of the decorating attribute. - /// - /// Renames the [`Ident`]s used in `attr` and stores the translation map in - /// `argument_names`. - fn new_ensures(sig: &Signature, mut attr: Expr) -> Self { - let argument_names = rename_argument_occurrences(sig, &mut attr); - ContractConditionsData::Ensures { argument_names, attr } - } - /// Constructs a [`Self::Modifies`] from the contents of the decorating attribute. /// /// Responsible for parsing the attribute. @@ -129,7 +124,10 @@ impl ContractConditionsData { /// - Creates new names for them; /// - Replaces all occurrences of those idents in `attrs` with the new names and; /// - Returns the mapping of old names to new names. -fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { +fn rename_argument_occurrences( + sig: &syn::Signature, + attr: &mut ExprClosure, +) -> HashMap { let mut arg_ident_collector = ArgumentIdentCollector::new(); arg_ident_collector.visit_signature(&sig); @@ -144,7 +142,7 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap .collect::>(); let mut ident_rewriter = Renamer(&arg_idents); - ident_rewriter.visit_expr_mut(attr); + ident_rewriter.visit_expr_closure_mut(attr); arg_idents } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 02d2b98eb8db..bef6f8d921bc 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -159,9 +159,9 @@ //! call_replace(fn args...) //! } else { //! unsafe { reentry = true }; -//! let result = call_check(fn args...); +//! let result_kani_internal = call_check(fn args...); //! unsafe { reentry = false }; -//! result +//! result_kani_internal //! } //! } //! ``` @@ -173,7 +173,7 @@ //! //! ``` //! #[kani::requires(divisor != 0)] -//! #[kani::ensures(result <= dividend)] +//! #[kani::ensures(|result : &u32| *result <= dividend)] //! fn div(dividend: u32, divisor: u32) -> u32 { //! dividend / divisor //! } @@ -186,31 +186,35 @@ //! #[kanitool::replaced_with = "div_replace_965916"] //! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } //! -//! #[allow(dead_code)] -//! #[allow(unused_variables)] -//! #[kanitool::is_contract_generated(check)] -//! fn div_check_965916(dividend: u32, divisor: u32) -> u32 { -//! let dividend_renamed = kani::internal::untracked_deref(÷nd); -//! let divisor_renamed = kani::internal::untracked_deref(&divisor); -//! let result = { kani::assume(divisor != 0); { dividend / divisor } }; -//! kani::assert(result <= dividend_renamed, "result <= dividend"); +//! #[allow(dead_code, unused_variables)] +//! #[kanitool :: is_contract_generated(check)] fn +//! div_check_b97df2(dividend : u32, divisor : u32) -> u32 +//! { +//! let dividend_renamed = kani::internal::untracked_deref(& dividend); +//! let divisor_renamed = kani::internal::untracked_deref(& divisor); +//! kani::assume(divisor != 0); +//! let result_kani_internal : u32 = div_wrapper_b97df2(dividend, divisor); +//! kani::assert( +//! (| result : & u32 | *result <= dividend_renamed)(& result_kani_internal), +//! stringify!(|result : &u32| *result <= dividend)); //! std::mem::forget(dividend_renamed); //! std::mem::forget(divisor_renamed); -//! result +//! result_kani_internal //! } //! -//! #[allow(dead_code)] -//! #[allow(unused_variables)] -//! #[kanitool::is_contract_generated(replace)] -//! fn div_replace_965916(dividend: u32, divisor: u32) -> u32 { -//! kani::assert(divisor != 0, "divisor != 0"); -//! let dividend_renamed = kani::internal::untracked_deref(÷nd); -//! let divisor_renamed = kani::internal::untracked_deref(&divisor); -//! let result = kani::any(); -//! kani::assume(result <= dividend_renamed, "result <= dividend"); -//! std::mem::forget(dividend_renamed); +//! #[allow(dead_code, unused_variables)] +//! #[kanitool :: is_contract_generated(replace)] fn +//! div_replace_b97df2(dividend : u32, divisor : u32) -> u32 +//! { +//! let divisor_renamed = kani::internal::untracked_deref(& divisor); +//! let dividend_renamed = kani::internal::untracked_deref(& dividend); +//! kani::assert(divisor != 0, stringify! (divisor != 0)); +//! let result_kani_internal : u32 = kani::any_modifies(); +//! kani::assume( +//! (|result : & u32| *result <= dividend_renamed)(&result_kani_internal)); //! std::mem::forget(divisor_renamed); -//! result +//! std::mem::forget(dividend_renamed); +//! result_kani_internal //! } //! //! #[allow(dead_code)] @@ -220,12 +224,12 @@ //! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { -//! div_replace_965916(dividend, divisor) +//! div_replace_b97df2(dividend, divisor) //! } else { //! unsafe { reentry = true }; -//! let result = div_check_965916(dividend, divisor); +//! let result_kani_internal = div_check_b97df2(dividend, divisor); //! unsafe { reentry = false }; -//! result +//! result_kani_internal //! } //! } //! ``` @@ -243,6 +247,8 @@ mod initialize; mod replace; mod shared; +const INTERNAL_RESULT_IDENT: &str = "result_kani_internal"; + pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { contract_main(attr, item, ContractConditionsType::Requires) } diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 28e401c22d48..546568dc8a1d 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -3,13 +3,13 @@ //! Logic used for generating the code that replaces a function with its contract. -use proc_macro2::{Ident, TokenStream as TokenStream2}; +use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; use super::{ helpers::*, shared::{make_unsafe_argument_copies, try_as_result_assign}, - ContractConditionsData, ContractConditionsHandler, + ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; impl<'a> ContractConditionsHandler<'a> { @@ -39,7 +39,8 @@ impl<'a> ContractConditionsHandler<'a> { fn ensure_bootstrapped_replace_body(&self) -> (Vec, Vec) { if self.is_first_emit() { let return_type = return_type_to_type(&self.annotated_fn.sig.output); - (vec![syn::parse_quote!(let result : #return_type = kani::any_modifies();)], vec![]) + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![]) } else { let stmts = &self.annotated_fn.block.stmts; let idx = stmts @@ -70,30 +71,33 @@ impl<'a> ContractConditionsHandler<'a> { match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( kani::assert(#attr, stringify!(#attr_copy)); #(#before)* #(#after)* - result + #result ) } ContractConditionsData::Ensures { attr, argument_names } => { let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #arg_copies #(#before)* #(#after)* kani::assume(#attr); #copy_clean - result + #result ) } ContractConditionsData::Modifies { attr } => { + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)* #(#after)* - result + #result ) } } @@ -126,7 +130,7 @@ impl<'a> ContractConditionsHandler<'a> { } } -/// Is this statement `let result : <...> = kani::any_modifies();`. +/// Is this statement `let result_kani_internal : <...> = kani::any_modifies();`. fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool { let Some(syn::LocalInit { diverge: None, expr: e, .. }) = try_as_result_assign(stmt) else { return false; diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index bf5a8000da50..b0f5804824ad 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -13,7 +13,7 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; use syn::Attribute; -use super::{ContractConditionsHandler, ContractFunctionState}; +use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; impl ContractFunctionState { /// Do we need to emit the `is_contract_generated` tag attribute on the @@ -114,7 +114,7 @@ macro_rules! try_as_result_assign_pat { ident: result_ident, subpat: None, .. - }) if result_ident == "result" + }) if result_ident == INTERNAL_RESULT_IDENT ) => init.$convert(), _ => None, } diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index dae805a7db72..deeeca66ab7a 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -65,7 +65,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { ```rs #[kani::requires(divisor != 0)] - #[kani::ensures(result <= dividend)] + #[kani::ensures(|result : &u32| *result <= dividend)] fn my_div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } @@ -79,8 +79,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { Conditions in contracts are Rust expressions which reference the function arguments and, in case of `ensures`, the return value of the - function. The return value is a special variable called `result` (see [open - questions](#open-questions) on a discussion about (re)naming). Syntactically + function. The return value is passed into the ensures closure statement by reference. Syntactically Kani supports any Rust expression, including function calls, defining types etc. However they must be side-effect free (see also side effects [here](#changes-to-other-components)) or Kani will throw a compile error. @@ -132,8 +131,8 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { let dividend = kani::any(); let divisor = kani::any(); kani::assume(divisor != 0); // requires - let result = my_div(dividend, divisor); - kani::assert(result <= dividend); // ensures + let result_kani_internal = my_div(dividend, divisor); + kani::assert((|result : &u32| *result <= dividend)(result_kani_internal)); // ensures } ``` @@ -306,7 +305,7 @@ available to `ensures`. It is used like so: ```rs impl Vec { - #[kani::ensures(old(self.is_empty()) || result.is_some())] + #[kani::ensures(|result : &Option| old(self.is_empty()) || result.is_some())] fn pop(&mut self) -> Option { ... } @@ -324,8 +323,8 @@ Note also that `old` is syntax, not a function and implemented as an extraction and lifting during code generation. It can reference e.g. `pop`'s arguments but not local variables. Compare the following -**Invalid ❌:** `#[kani::ensures({ let x = self.is_empty(); old(x) } || result.is_some())]`
-**Valid ✅:** `#[kani::ensures(old({ let x = self.is_empty(); x }) || result.is_some())]` +**Invalid ❌:** `#[kani::ensures(|result : &Option| { let x = self.is_empty(); old(x) } || result.is_some())]`
+**Valid ✅:** `#[kani::ensures(|result : &Option| old({ let x = self.is_empty(); x }) || result.is_some())]` And it will only be recognized as `old(...)`, not as `let old1 = old; old1(...)` etc. @@ -410,7 +409,7 @@ the below example: ```rs impl Vec { - #[kani::ensures(self.is_empty() || self.len() == old(self.len()) - 1)] + #[kani::ensures(|result : &Option| self.is_empty() || self.len() == old(self.len()) - 1)] fn pop(&mut self) -> Option { ... } @@ -425,8 +424,8 @@ following: impl Vec { fn check_pop(&mut self) -> Option { let old_1 = self.len(); - let result = Self::pop(self); - kani::assert(self.is_empty() || self.len() == old_1 - 1) + let result_kani_internal = Self::pop(self); + kani::assert((|result : &Option| self.is_empty() || self.len() == old_1 - 1)(result_kani_internal)) } } ``` @@ -450,7 +449,7 @@ sensible contract for it might look as follows: ```rs impl Vec { - #[ensures(self.len() == result.0.len() + result.1.len())] + #[ensures(|result : &(&mut [T], &mut [T])| self.len() == result.0.len() + result.1.len())] fn split_at_mut(&mut self, i: usize) -> (&mut [T], &mut [T]) { ... } diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected index 0a59d2cea5eb..4b70f8364e05 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.expected +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -1,6 +1,6 @@ assertion\ - Status: FAILURE\ -- Description: "result == x"\ +- Description: "|result : &u32| *result == x"\ in function max VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs index 91638b1cc037..8d66402180d7 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.rs +++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(result == x)] +#[kani::ensures(|result : &u32| *result == x)] fn max(x: u32, y: u32) -> u32 { if x > y { x } else { y } } diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected index 85619fa84c22..9eee213789b9 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.expected +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "result == x || result == y"\ +- Description: "|result : &u32| *result == x || *result == y"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs index df8d3a2361fb..86302f705925 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.rs +++ b/tests/expected/function-contract/arbitrary_ensures_pass.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(result == x || result == y)] +#[kani::ensures(|result : &u32| *result == x || *result == y)] fn max(x: u32, y: u32) -> u32 { if x > y { x } else { y } } diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs index d052e19b0335..78ab1b77bf10 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.rs +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(result <= dividend)] +#[kani::ensures(|result : &u32| *result <= dividend)] fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } diff --git a/tests/expected/function-contract/attribute_complain.rs b/tests/expected/function-contract/attribute_complain.rs index f16e975c2001..8532889e1eca 100644 --- a/tests/expected/function-contract/attribute_complain.rs +++ b/tests/expected/function-contract/attribute_complain.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn always() {} #[kani::proof_for_contract(always)] diff --git a/tests/expected/function-contract/attribute_no_complain.rs b/tests/expected/function-contract/attribute_no_complain.rs index bcf1f0cadafd..b3004b24f4d4 100644 --- a/tests/expected/function-contract/attribute_no_complain.rs +++ b/tests/expected/function-contract/attribute_no_complain.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn always() {} #[kani::proof] diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected index c31b5c389fc8..e181e6b2ad17 100644 --- a/tests/expected/function-contract/checking_from_external_mod.expected +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -1,5 +1,5 @@ - Status: SUCCESS\ -- Description: "(result == x) | (result == y)"\ +- Description: "|result : &u32| (*result == x) | (*result == y)"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_from_external_mod.rs b/tests/expected/function-contract/checking_from_external_mod.rs index 43d1551f9aef..ea01cfadd511 100644 --- a/tests/expected/function-contract/checking_from_external_mod.rs +++ b/tests/expected/function-contract/checking_from_external_mod.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures((result == x) | (result == y))] +#[kani::ensures(|result : &u32| (*result == x) | (*result == y))] fn max(x: u32, y: u32) -> u32 { if x > y { x } else { y } } diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected index d5a390be8425..cfe84c06fc85 100644 --- a/tests/expected/function-contract/checking_in_impl.expected +++ b/tests/expected/function-contract/checking_in_impl.expected @@ -1,5 +1,5 @@ - Status: SUCCESS\ -- Description: "(result == self) | (result == y)"\ +- Description: "|result : &WrappedInt| (*result == self) | (*result == y)"\ in function WrappedInt::max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_in_impl.rs b/tests/expected/function-contract/checking_in_impl.rs index 7d5c0506d9df..8721e7fffb7f 100644 --- a/tests/expected/function-contract/checking_in_impl.rs +++ b/tests/expected/function-contract/checking_in_impl.rs @@ -8,7 +8,7 @@ extern crate kani; struct WrappedInt(u32); impl WrappedInt { - #[kani::ensures((result == self) | (result == y))] + #[kani::ensures(|result : &WrappedInt| (*result == self) | (*result == y))] fn max(self, y: WrappedInt) -> WrappedInt { Self(if self.0 > y.0 { self.0 } else { y.0 }) } diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected index 32fc28012d3a..79cc3d572af0 100644 --- a/tests/expected/function-contract/fail_on_two.expected +++ b/tests/expected/function-contract/fail_on_two.expected @@ -7,6 +7,6 @@ Failed Checks: internal error: entered unreachable code: fail on two assertion\ - Status: FAILURE\ -- Description: "result < 3" +- Description: "|result : &i32| *result < 3" -Failed Checks: result < 3 +Failed Checks: |result : &i32| *result < 3 diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs index 605065449194..32ad74c31cd9 100644 --- a/tests/expected/function-contract/fail_on_two.rs +++ b/tests/expected/function-contract/fail_on_two.rs @@ -16,7 +16,7 @@ //! once because the postcondition is violated). If instead the hypothesis (e.g. //! contract replacement) is used we'd expect the verification to succeed. -#[kani::ensures(result < 3)] +#[kani::ensures(|result : &i32| *result < 3)] #[kani::recursion] fn fail_on_two(i: i32) -> i32 { match i { @@ -32,7 +32,7 @@ fn harness() { let _ = fail_on_two(first); } -#[kani::ensures(result < 3)] +#[kani::ensures(|result : &i32| *result < 3)] #[kani::recursion] fn fail_on_two_in_postcondition(i: i32) -> i32 { let j = i + 1; diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected index c7fe5a721abb..ca21817c8329 100644 --- a/tests/expected/function-contract/gcd_failure_code.expected +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -1,8 +1,8 @@ assertion\ - Status: FAILURE\ -- Description: "result != 0 && x % result == 0 && y % result == 0"\ +- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\ in function gcd -Failed Checks: result != 0 && x % result == 0 && y % result == 0 +Failed Checks: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_failure_code.rs b/tests/expected/function-contract/gcd_failure_code.rs index f76e04b75fee..118cc3c930e5 100644 --- a/tests/expected/function-contract/gcd_failure_code.rs +++ b/tests/expected/function-contract/gcd_failure_code.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected index aeadfb563ab9..4bb02ab36f49 100644 --- a/tests/expected/function-contract/gcd_failure_contract.expected +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -1,8 +1,8 @@ assertion\ - Status: FAILURE\ -- Description: "result != 0 && x % result == 1 && y % result == 0"\ +- Description: "|result : &T| *result != 0 && x % *result == 1 && y % *result == 0"\ in function gcd\ -Failed Checks: result != 0 && x % result == 1 && y % result == 0 +Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_failure_contract.rs b/tests/expected/function-contract/gcd_failure_contract.rs index 6b835466c5a0..d4eea8ceb98c 100644 --- a/tests/expected/function-contract/gcd_failure_contract.rs +++ b/tests/expected/function-contract/gcd_failure_contract.rs @@ -5,8 +5,8 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -// Changed `0` to `1` in `x % result == 0` to mess with this contract -#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] +// Changed `0` to `1` in `x % *result == 0` to mess with this contract +#[kani::ensures(|result : &T| *result != 0 && x % *result == 1 && y % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/gcd_rec_code_fail.expected b/tests/expected/function-contract/gcd_rec_code_fail.expected index 80dbaadbf4c7..863392098be4 100644 --- a/tests/expected/function-contract/gcd_rec_code_fail.expected +++ b/tests/expected/function-contract/gcd_rec_code_fail.expected @@ -1,3 +1,3 @@ -Failed Checks: result != 0 && x % result == 0 && y % result == 0 +Failed Checks: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_code_fail.rs b/tests/expected/function-contract/gcd_rec_code_fail.rs index da38318e2a66..90260f56d4dc 100644 --- a/tests/expected/function-contract/gcd_rec_code_fail.rs +++ b/tests/expected/function-contract/gcd_rec_code_fail.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] #[kani::recursion] fn gcd(x: T, y: T) -> T { let mut max = x; diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected index da647dfd40aa..0556bfc50204 100644 --- a/tests/expected/function-contract/gcd_rec_comparison_pass.expected +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected @@ -4,6 +4,6 @@ assertion\ assertion\ - Status: SUCCESS\ -- Description: "result != 0 && x % result == 0 && y % result == 0" +- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.rs b/tests/expected/function-contract/gcd_rec_comparison_pass.rs index 1db9691ae8e4..ae5fbbe9b60f 100644 --- a/tests/expected/function-contract/gcd_rec_comparison_pass.rs +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] #[kani::recursion] fn gcd(x: T, y: T) -> T { let mut max = x; diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.expected b/tests/expected/function-contract/gcd_rec_contract_fail.expected index bfb470192a39..6cc0354ca89a 100644 --- a/tests/expected/function-contract/gcd_rec_contract_fail.expected +++ b/tests/expected/function-contract/gcd_rec_contract_fail.expected @@ -1,3 +1,3 @@ -Failed Checks: result != 0 && x % result == 1 && y % result == 0 +Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0 VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.rs b/tests/expected/function-contract/gcd_rec_contract_fail.rs index 3fe34cb2effc..2306db0e9353 100644 --- a/tests/expected/function-contract/gcd_rec_contract_fail.rs +++ b/tests/expected/function-contract/gcd_rec_contract_fail.rs @@ -6,7 +6,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] // Changed `0` to `1` in `x % result == 0` to mess with this contract -#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 1 && y % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs index d8a5bbd234ed..0fd04b0076ba 100644 --- a/tests/expected/function-contract/gcd_rec_replacement_pass.rs +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected index da647dfd40aa..0556bfc50204 100644 --- a/tests/expected/function-contract/gcd_rec_simple_pass.expected +++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected @@ -4,6 +4,6 @@ assertion\ assertion\ - Status: SUCCESS\ -- Description: "result != 0 && x % result == 0 && y % result == 0" +- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.rs b/tests/expected/function-contract/gcd_rec_simple_pass.rs index 464e3d8bbea1..626a48aa5ec2 100644 --- a/tests/expected/function-contract/gcd_rec_simple_pass.rs +++ b/tests/expected/function-contract/gcd_rec_simple_pass.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] #[kani::recursion] fn gcd(x: T, y: T) -> T { let mut max = x; diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs index 8bd59c5c14fe..0186a369c3b2 100644 --- a/tests/expected/function-contract/gcd_replacement_fail.rs +++ b/tests/expected/function-contract/gcd_replacement_fail.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs index 9827dd3a1512..b45241198737 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.rs +++ b/tests/expected/function-contract/gcd_replacement_pass.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected index 73b531d424b9..e5885dd11179 100644 --- a/tests/expected/function-contract/gcd_success.expected +++ b/tests/expected/function-contract/gcd_success.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "result != 0 && x % result == 0 && y % result == 0"\ +- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\ in function gcd VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs index d3a2c75b7d20..3b983a230b60 100644 --- a/tests/expected/function-contract/gcd_success.rs +++ b/tests/expected/function-contract/gcd_success.rs @@ -5,7 +5,7 @@ type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] fn gcd(x: T, y: T) -> T { let mut max = x; let mut min = y; diff --git a/tests/expected/function-contract/modifies/check_only_verification.rs b/tests/expected/function-contract/modifies/check_only_verification.rs index 2f247a718ae9..9f3fb3614733 100644 --- a/tests/expected/function-contract/modifies/check_only_verification.rs +++ b/tests/expected/function-contract/modifies/check_only_verification.rs @@ -7,7 +7,7 @@ #[kani::requires(*ptr < 100)] #[kani::modifies(ptr)] -#[kani::ensures(result == 100)] +#[kani::ensures(|result : &u32| *result == 100)] fn modify(ptr: &mut u32) -> u32 { *ptr += 1; *ptr diff --git a/tests/expected/function-contract/modifies/expr_pass.rs b/tests/expected/function-contract/modifies/expr_pass.rs index 65e561df48a2..9a6f46a6aaaa 100644 --- a/tests/expected/function-contract/modifies/expr_pass.rs +++ b/tests/expected/function-contract/modifies/expr_pass.rs @@ -7,7 +7,7 @@ #[kani::requires(**ptr < 100)] #[kani::modifies(ptr.as_ref())] -#[kani::ensures(**ptr < 101)] +#[kani::ensures(|result| **ptr < 101)] fn modify(ptr: &mut Box) { *ptr.as_mut() += 1; } diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.rs b/tests/expected/function-contract/modifies/expr_replace_pass.rs index 8be1ef2cbaee..779280dd46b4 100644 --- a/tests/expected/function-contract/modifies/expr_replace_pass.rs +++ b/tests/expected/function-contract/modifies/expr_replace_pass.rs @@ -4,7 +4,7 @@ #[kani::requires(**ptr < 100)] #[kani::modifies(ptr.as_ref())] -#[kani::ensures(**ptr == prior + 1)] +#[kani::ensures(|result| **ptr == prior + 1)] fn modify(ptr: &mut Box, prior: u32) { *ptr.as_mut() += 1; } diff --git a/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs b/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs index 644b641e731e..5e9b96e021f7 100644 --- a/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs +++ b/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs @@ -5,7 +5,7 @@ //! Check whether Kani fails if users forgot to annotate recursive //! functions with `#[kani::recursion]` when using function contracts. -#[kani::ensures(result < 3)] +#[kani::ensures(|result : &i32| *result < 3)] fn fail_on_two(i: i32) -> i32 { match i { 0 => fail_on_two(i + 1), diff --git a/tests/expected/function-contract/modifies/field_replace_pass.rs b/tests/expected/function-contract/modifies/field_replace_pass.rs index a6ae4ea4a7e0..1bbbaf31121a 100644 --- a/tests/expected/function-contract/modifies/field_replace_pass.rs +++ b/tests/expected/function-contract/modifies/field_replace_pass.rs @@ -8,7 +8,7 @@ struct S<'a> { } #[kani::requires(*s.target < 100)] #[kani::modifies(s.target)] -#[kani::ensures(*s.target == prior + 1)] +#[kani::ensures(|result| *s.target == prior + 1)] fn modify(s: S, prior: u32) { *s.target += 1; } diff --git a/tests/expected/function-contract/modifies/global_replace_pass.rs b/tests/expected/function-contract/modifies/global_replace_pass.rs index 333348f25ce4..69d36bd96033 100644 --- a/tests/expected/function-contract/modifies/global_replace_pass.rs +++ b/tests/expected/function-contract/modifies/global_replace_pass.rs @@ -5,7 +5,7 @@ static mut PTR: u32 = 0; #[kani::modifies(&mut PTR)] -#[kani::ensures(PTR == src)] +#[kani::ensures(|result| PTR == src)] unsafe fn modify(src: u32) { PTR = src; } diff --git a/tests/expected/function-contract/modifies/havoc_pass.rs b/tests/expected/function-contract/modifies/havoc_pass.rs index aa5bcada1a26..ebdd139727d3 100644 --- a/tests/expected/function-contract/modifies/havoc_pass.rs +++ b/tests/expected/function-contract/modifies/havoc_pass.rs @@ -3,7 +3,7 @@ // kani-flags: -Zfunction-contracts #[kani::modifies(dst)] -#[kani::ensures(*dst == src)] +#[kani::ensures(|result| *dst == src)] fn copy(src: u32, dst: &mut u32) { *dst = src; } diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs index dc5f370179e5..43581ee677a6 100644 --- a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs @@ -3,7 +3,7 @@ // kani-flags: -Zfunction-contracts // These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still -#[kani::ensures(*dst == src)] +#[kani::ensures(|result| *dst == src)] #[kani::modifies(dst)] fn copy(src: u32, dst: &mut u32) { *dst = src; diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.rs b/tests/expected/function-contract/modifies/mistake_condition_return.rs index 484819af4248..b2d6ad6a8a55 100644 --- a/tests/expected/function-contract/modifies/mistake_condition_return.rs +++ b/tests/expected/function-contract/modifies/mistake_condition_return.rs @@ -16,8 +16,8 @@ // However, contract instrumentation will create a separate non-deterministic // value to return in this function that can only be constrained by using the // `result` keyword. Thus the correct condition would be -// `#[kani::ensures(result == 100)]`. -#[kani::ensures(*ptr == 100)] +// `#[kani::ensures(|result| result == 100)]`. +#[kani::ensures(|result| *ptr == 100)] fn modify(ptr: &mut u32) -> u32 { *ptr += 1; *ptr diff --git a/tests/expected/function-contract/modifies/unique_arguments.rs b/tests/expected/function-contract/modifies/unique_arguments.rs index 396ba4c5b036..ea4502bde2ad 100644 --- a/tests/expected/function-contract/modifies/unique_arguments.rs +++ b/tests/expected/function-contract/modifies/unique_arguments.rs @@ -4,8 +4,8 @@ #[kani::modifies(a)] #[kani::modifies(b)] -#[kani::ensures(*a == 1)] -#[kani::ensures(*b == 2)] +#[kani::ensures(|result| *a == 1)] +#[kani::ensures(|result| *b == 2)] fn two_pointers(a: &mut u32, b: &mut u32) { *a = 1; *b = 2; diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected index d31486f2dcc6..4d5407fdd850 100644 --- a/tests/expected/function-contract/modifies/vec_pass.expected +++ b/tests/expected/function-contract/modifies/vec_pass.expected @@ -15,6 +15,6 @@ in function modify_replace assertion\ - Status: SUCCESS\ -- Description: "v[0] == src" +- Description: "|result| v[0] == src" VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass.rs index 1e40a2a08eb7..e3ac28ac3b3d 100644 --- a/tests/expected/function-contract/modifies/vec_pass.rs +++ b/tests/expected/function-contract/modifies/vec_pass.rs @@ -4,7 +4,7 @@ #[kani::requires(v.len() > 0)] #[kani::modifies(&v[0])] -#[kani::ensures(v[0] == src)] +#[kani::ensures(|result| v[0] == src)] fn modify(v: &mut Vec, src: u32) { v[0] = src } diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs index a51312acd2f0..ead1c1538b4d 100644 --- a/tests/expected/function-contract/pattern_use.rs +++ b/tests/expected/function-contract/pattern_use.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(result <= dividend)] +#[kani::ensures(|result : &u32| *result <= dividend)] fn div((dividend, divisor): (u32, u32)) -> u32 { dividend / divisor } diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs index 3d88fc0926ed..1b3653951ad1 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs @@ -4,7 +4,7 @@ #![allow(unreachable_code, unused_variables)] -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn allowed_pointer(t: *const bool) {} #[kani::proof_for_contract(allowed_pointer)] diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs index 22771f76632d..2c41bf28d741 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs @@ -4,7 +4,7 @@ #![allow(unreachable_code, unused_variables)] -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn allowed_mut_ref(t: &mut bool) {} #[kani::proof_for_contract(allowed_mut_ref)] diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs index e5151396898d..fdab681e0c05 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs @@ -17,7 +17,7 @@ impl<'a> kani::Arbitrary for ArbitraryPointer<&'a mut bool> { } } -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn allowed_mut_return_ref<'a>() -> ArbitraryPointer<&'a mut bool> { ArbitraryPointer(unsafe { &mut B as &'a mut bool }) } diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs index 3dd4145eff9c..cef3e87ee0f2 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs @@ -4,7 +4,7 @@ #![allow(unreachable_code, unused_variables)] -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn allowed_ref(t: &bool) {} #[kani::proof_for_contract(allowed_ref)] diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.rs b/tests/expected/function-contract/prohibit-pointers/hidden.rs index 9ca23fe6b2e1..1a9b7a475479 100644 --- a/tests/expected/function-contract/prohibit-pointers/hidden.rs +++ b/tests/expected/function-contract/prohibit-pointers/hidden.rs @@ -6,7 +6,7 @@ struct HidesAPointer(*mut u32); -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn hidden_pointer(h: HidesAPointer) {} #[kani::proof_for_contract(hidden_pointer)] diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs index 24e9d006a9c0..868327e15046 100644 --- a/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs +++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs @@ -4,7 +4,7 @@ #![allow(unreachable_code, unused_variables)] -#[kani::ensures(true)] +#[kani::ensures(|result| true)] fn plain_pointer(t: *mut i32) {} #[kani::proof_for_contract(plain_pointer)] diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs index 2bacdca9bbb6..6314129ddf89 100644 --- a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(unsafe{ *result == *input })] +#[kani::ensures(|result : &*const usize| unsafe{ **result == *input })] fn return_pointer(input: *const usize) -> *const usize { input } diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected index 8e9b42d42640..360242d07daf 100644 --- a/tests/expected/function-contract/simple_ensures_fail.expected +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -1,8 +1,8 @@ assertion\ - Status: FAILURE\ -- Description: "result == x"\ +- Description: "|result : &u32| *result == x"\ in function max -Failed Checks: result == x +Failed Checks: |result : &u32| *result == x VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs index 687853612dcc..43521b171ea7 100644 --- a/tests/expected/function-contract/simple_ensures_fail.rs +++ b/tests/expected/function-contract/simple_ensures_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(result == x)] +#[kani::ensures(|result : &u32| *result == x)] fn max(x: u32, y: u32) -> u32 { if x > y { x } else { y } } diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected index 5a7874964413..bdcde74c3bfe 100644 --- a/tests/expected/function-contract/simple_ensures_pass.expected +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -1,6 +1,6 @@ assertion\ - Status: SUCCESS\ -- Description: "(result == x) | (result == y)"\ +- Description: "|result : &u32| (*result == x) | (*result == y)"\ in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs index 2d36f5c96e88..7be58fef3b04 100644 --- a/tests/expected/function-contract/simple_ensures_pass.rs +++ b/tests/expected/function-contract/simple_ensures_pass.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures((result == x) | (result == y))] +#[kani::ensures(|result : &u32| (*result == x) | (*result == y))] fn max(x: u32, y: u32) -> u32 { if x > y { x } else { y } } diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs index 33a531a3aef7..dd448d2cdee6 100644 --- a/tests/expected/function-contract/simple_replace_fail.rs +++ b/tests/expected/function-contract/simple_replace_fail.rs @@ -3,7 +3,7 @@ // kani-flags: -Zfunction-contracts #[kani::requires(divisor != 0)] -#[kani::ensures(result <= dividend)] +#[kani::ensures(|result : &u32| *result <= dividend)] fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs index 0dcc6cd59fe3..7c57cc6a0b7f 100644 --- a/tests/expected/function-contract/simple_replace_pass.rs +++ b/tests/expected/function-contract/simple_replace_pass.rs @@ -3,7 +3,7 @@ // kani-flags: -Zfunction-contracts #[kani::requires(divisor != 0)] -#[kani::ensures(result <= dividend)] +#[kani::ensures(|result : &u32| *result <= dividend)] fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs index 09b20443d47b..5a3b9fbae5b0 100644 --- a/tests/expected/function-contract/type_annotation_needed.rs +++ b/tests/expected/function-contract/type_annotation_needed.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#[kani::ensures(result.is_some())] +#[kani::ensures(|result : &Option| result.is_some())] fn or_default(opt: Option) -> Option { opt.or(Some(T::default())) } diff --git a/tests/std-checks/core/src/ptr.rs b/tests/std-checks/core/src/ptr.rs index 847b8fd1c138..49cf9e168214 100644 --- a/tests/std-checks/core/src/ptr.rs +++ b/tests/std-checks/core/src/ptr.rs @@ -9,8 +9,8 @@ pub mod contracts { use super::*; use kani::{ensures, implies, mem::*, modifies, requires}; - #[ensures(implies!(ptr.is_null() => result.is_none()))] - #[ensures(implies!(!ptr.is_null() => result.is_some()))] + #[ensures(|result : &Option>| implies!(ptr.is_null() => result.is_none()))] + #[ensures(|result : &Option>| implies!(!ptr.is_null() => result.is_some()))] pub fn new(ptr: *mut T) -> Option> { NonNull::new(ptr) }