Box validity: update for new zero-sized rules · patricklam/verify-rust-std@228ec9e (original) (raw)
`@@ -53,22 +53,19 @@
`
53
53
`//!
`
54
54
`//! # Memory layout
`
55
55
`//!
`
56
``
`` -
//! For non-zero-sized values, a [Box] will use the [Global] allocator for
``
57
``
`` -
//! its allocation. It is valid to convert both ways between a [Box] and a
``
58
``
`` -
//! raw pointer allocated with the [Global] allocator, given that the
``
59
``
`` -
//! [Layout] used with the allocator is correct for the type. More precisely,
``
60
``
`` -
//! a value: *mut T that has been allocated with the [Global] allocator
``
61
``
`` -
//! with Layout::for_value(&*value) may be converted into a box using
``
62
``
`` -
//! [Box::<T>::from_raw(value)]. Conversely, the memory backing a `value: *mut
``
63
``
`` -
//! T obtained from [Box::::into_raw`] may be deallocated using the
``
64
``
`` -
//! [Global] allocator with [Layout::for_value(&*value)].
``
``
56
`` +
//! For non-zero-sized values, a [Box] will use the [Global] allocator for its allocation. It is
``
``
57
`` +
//! valid to convert both ways between a [Box] and a raw pointer allocated with the [Global]
``
``
58
`` +
//! allocator, given that the [Layout] used with the allocator is correct for the type and the raw
``
``
59
`` +
//! pointer points to a valid value of the right type. More precisely, a value: *mut T that has
``
``
60
`` +
//! been allocated with the [Global] allocator with Layout::for_value(&*value) may be converted
``
``
61
`` +
//! into a box using [Box::<T>::from_raw(value)]. Conversely, the memory backing a value: *mut T
``
``
62
`` +
//! obtained from [Box::<T>::into_raw] may be deallocated using the [Global] allocator with
``
``
63
`` +
//! [Layout::for_value(&*value)].
``
65
64
`//!
`
66
``
`` -
//! For zero-sized values, the Box pointer still has to be [valid] for reads
``
67
``
`-
//! and writes and sufficiently aligned. In particular, casting any aligned
`
68
``
`-
//! non-zero integer literal to a raw pointer produces a valid pointer, but a
`
69
``
`-
//! pointer pointing into previously allocated memory that since got freed is
`
70
``
`` -
//! not valid. The recommended way to build a Box to a ZST if Box::new cannot
``
71
``
`` -
//! be used is to use [ptr::NonNull::dangling].
``
``
65
`` +
//! For zero-sized values, the Box pointer has to be non-null and sufficiently aligned. The
``
``
66
`` +
//! recommended way to build a Box to a ZST if Box::new cannot be used is to use
``
``
67
`` +
//! [ptr::NonNull::dangling]. Even for zero-sized types, the pointee type must be inhabited
``
``
68
`+
//! to ensure that the Box points to a valid value of the given type.
`
72
69
`//!
`
73
70
`` //! So long as T: Sized, a Box<T> is guaranteed to be represented
``
74
71
`//! as a single pointer and is also ABI-compatible with C pointers
`