diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index c893c386ee5d..90fda5ac90b5 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -225,4 +225,4 @@ //! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T` //! must implement [`Arbitrary`](super::Arbitrary). This is used to assign //! `kani::any()` to the location when the function is used in a `stub_verified`. -pub use super::{ensures, proof_for_contract, requires, stub_verified, modifies}; +pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified}; diff --git a/tests/expected/function-contract/modifies/unique_arguments.rs b/tests/expected/function-contract/modifies/unique_arguments.rs index a0f034cd12c8..396ba4c5b036 100644 --- a/tests/expected/function-contract/modifies/unique_arguments.rs +++ b/tests/expected/function-contract/modifies/unique_arguments.rs @@ -11,13 +11,11 @@ fn two_pointers(a: &mut u32, b: &mut u32) { *b = 2; } - #[kani::proof_for_contract(two_pointers)] fn test_contract() { two_pointers(&mut kani::any(), &mut kani::any()); } - #[kani::proof] #[kani::stub_verified(two_pointers)] fn test_stubbing() {