From d640ef60c9c17ac5c72b49facc833cd3be1879de Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Oct 2024 13:30:31 +0000 Subject: [PATCH] Disable check_grow_impl as we cannot currently express the necessary precondition --- library/alloc/src/alloc.rs | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index a198531104ff4..44b1c680c5e9b 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -459,15 +459,17 @@ mod verify { let _ = Global.alloc_impl(kani::any(), kani::any()); } - // unsafe fn grow_impl(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result, AllocError> - #[kani::proof_for_contract(Global::grow_impl)] - pub fn check_grow_impl() { - let raw_ptr = kani::any::() as *mut u8; - unsafe { - let n = NonNull::new_unchecked(raw_ptr); - let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any()); - } - } + // TODO: Kani correctly detects that the precondition is too weak. We'd need a way to express + // that ptr either points to a ZST (we can do this), or else is heap-allocated (we cannot). + // // unsafe fn grow_impl(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result, AllocError> + // #[kani::proof_for_contract(Global::grow_impl)] + // pub fn check_grow_impl() { + // let raw_ptr = kani::any::() as *mut u8; + // unsafe { + // let n = NonNull::new_unchecked(raw_ptr); + // let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any()); + // } + // } // TODO: disabled as Kani does not currently support contracts on traits. See // https://github.com/model-checking/kani/issues/1997