restate GlobalAlloc method safety preconditions in terms of what the … · qinheping/verify-rust-std@9469575 (original) (raw)
`@@ -124,8 +124,8 @@ pub unsafe trait GlobalAlloc {
`
124
124
`///
`
125
125
`/// # Safety
`
126
126
`///
`
127
``
`-
/// This function is unsafe because undefined behavior can result
`
128
``
`` -
/// if the caller does not ensure that layout has non-zero size.
``
``
127
`` +
/// layout must have non-zero size. Attempting to allocate for a zero-sized layout may
``
``
128
`+
/// result in undefined behavior.
`
129
129
`///
`
130
130
`/// (Extension subtraits might provide more specific bounds on
`
131
131
`/// behavior, e.g., guarantee a sentinel address or a null pointer
`
`@@ -156,14 +156,14 @@ pub unsafe trait GlobalAlloc {
`
156
156
`///
`
157
157
`/// # Safety
`
158
158
`///
`
159
``
`-
/// This function is unsafe because undefined behavior can result
`
160
``
`-
/// if the caller does not ensure all of the following:
`
``
159
`+
/// The caller must ensure:
`
161
160
`///
`
162
``
`` -
/// * ptr must denote a block of memory currently allocated via
``
163
``
`-
/// this allocator,
`
``
161
`` +
/// * ptr is a block of memory currently allocated via this allocator and,
``
164
162
`///
`
165
``
`` -
/// * layout must be the same layout that was used
``
166
``
`-
/// to allocate that block of memory.
`
``
163
`` +
/// * layout is the same layout that was used to allocate that block of
``
``
164
`+
/// memory.
`
``
165
`+
///
`
``
166
`+
/// Otherwise undefined behavior can result.
`
167
167
`#[stable(feature = "global_alloc", since = "1.28.0")]
`
168
168
`unsafe fn dealloc(&self, ptr: *mut u8, layout: Layout);
`
169
169
``
`@@ -172,7 +172,8 @@ pub unsafe trait GlobalAlloc {
`
172
172
`///
`
173
173
`/// # Safety
`
174
174
`///
`
175
``
`` -
/// This function is unsafe for the same reasons that alloc is.
``
``
175
`` +
/// The caller has to ensure that layout has non-zero size. Like alloc
``
``
176
`` +
/// zero sized layout can result in undefined behaviour.
``
176
177
`/// However the allocated block of memory is guaranteed to be initialized.
`
177
178
`///
`
178
179
`/// # Errors
`
`@@ -220,20 +221,21 @@ pub unsafe trait GlobalAlloc {
`
220
221
`///
`
221
222
`/// # Safety
`
222
223
`///
`
223
``
`-
/// This function is unsafe because undefined behavior can result
`
224
``
`-
/// if the caller does not ensure all of the following:
`
``
224
`+
/// The caller must ensure that:
`
225
225
`///
`
226
``
`` -
/// * ptr must be currently allocated via this allocator,
``
``
226
`` +
/// * ptr is allocated via this allocator,
``
227
227
`///
`
228
``
`` -
/// * layout must be the same layout that was used
``
``
228
`` +
/// * layout is the same layout that was used
``
229
229
`/// to allocate that block of memory,
`
230
230
`///
`
231
``
`` -
/// * new_size must be greater than zero.
``
``
231
`` +
/// * new_size is greater than zero.
``
232
232
`///
`
233
233
`` /// * new_size, when rounded up to the nearest multiple of layout.align(),
``
234
``
`` -
/// must not overflow isize (i.e., the rounded value must be less than or
``
``
234
`` +
/// does not overflow isize (i.e., the rounded value must be less than or
``
235
235
`` /// equal to isize::MAX).
``
236
236
`///
`
``
237
`+
/// If these are not followed, undefined behaviour can result.
`
``
238
`+
///
`
237
239
`/// (Extension subtraits might provide more specific bounds on
`
238
240
`/// behavior, e.g., guarantee a sentinel address or a null pointer
`
239
241
`/// in response to a zero-size allocation request.)
`