From 41635f04bc5da95378ceb7f09a7152071dd449c0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 12:58:15 +0000 Subject: [PATCH] More on for_value, for_value_raw --- library/core/src/alloc/layout.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 4d38c1728fda2..a947812b7d6fb 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -177,7 +177,8 @@ impl Layout { #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")] #[must_use] #[inline] - #[ensures(|result| result.align().is_power_of_two())] + #[requires(mem::align_of_val(t).is_power_of_two())] + #[ensures(|result| result.align() == mem::align_of_val(t))] pub const fn for_value(t: &T) -> Self { let (size, align) = (mem::size_of_val(t), mem::align_of_val(t)); // SAFETY: see rationale in `new` for why this is using the unsafe variant @@ -596,15 +597,23 @@ mod verify { // pub const fn for_value(t: &T) -> Self #[kani::proof_for_contract(Layout::for_value)] pub fn check_for_value_i32() { + let x = kani::any::(); + let _ = Layout::for_value::(&x); let array : [i32; 2] = [1, 2]; let _ = Layout::for_value::<[i32]>(&array[1 .. 1]); + // TODO: the case of a trait object as unsized tail is not yet covered + // TODO: the case of an extern type as unsized tail is not yet covered } // pub const unsafe fn for_value_raw(t: *const T) -> Self #[kani::proof_for_contract(Layout::for_value_raw)] pub fn check_for_value_raw_i32() { unsafe { + let x = kani::any::(); + let _ = Layout::for_value_raw::(&x as *const i32); let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]); + // TODO: the case of a trait object as unsized tail is not yet covered + // TODO: the case of an extern type as unsized tail is not yet covered } }