From 351e958c1a5601b704343a34a44e66cd03c5cdc0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Sep 2024 14:00:13 -0400 Subject: [PATCH] Fix check_cast harness (#86) Modifies the `check_cast` harness to: - Be a proof instead of a proof for contract - Remove the generic type parameter Currently, Kani doesn't run this harness. (See the [log](https://github.com/model-checking/verify-rust-std/actions/runs/10887990165/job/30211482361?pr=85) from a recent PR). It doesn't run the harness because it has a generic type parameter, and Kani's error handling for contract proofs doesn't check for this condition. (PR to fix is [here](https://github.com/model-checking/kani/pull/3522)). Once we remove the generic type parameter so that the harness runs, Kani complains that we can't run it as a proof for contract because there are no contracts, so we make it a regular proof instead. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/ptr/unique.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs index edc1dc941cbc1..8a282c86a7868 100644 --- a/library/core/src/ptr/unique.rs +++ b/library/core/src/ptr/unique.rs @@ -284,8 +284,8 @@ mod verify { } // pub const fn cast(self) -> Unique - #[kani::proof_for_contract(Unique::cast)] - pub fn check_cast() { + #[kani::proof] + pub fn check_cast() { let mut x : i32 = kani::any(); let xptr = &mut x; unsafe {