Update NonNull::align_offset quarantees · patricklam/verify-rust-std@65c6173 (original) (raw)

`@@ -1171,16 +1171,23 @@ impl<T: ?Sized> NonNull {

`

1171

1171

`` /// align.

``

1172

1172

`///

`

1173

1173

`/// If it is not possible to align the pointer, the implementation returns

`

1174

``

`` -

/// usize::MAX. It is permissible for the implementation to always

``

1175

``

`` -

/// return usize::MAX. Only your algorithm's performance can depend

``

1176

``

`-

/// on getting a usable offset here, not its correctness.

`

``

1174

`` +

/// usize::MAX.

``

1177

1175

`///

`

1178

1176

`` /// The offset is expressed in number of T elements, and not bytes.

``

1179

1177

`///

`

1180

1178

`/// There are no guarantees whatsoever that offsetting the pointer will not overflow or go

`

1181

1179

`/// beyond the allocation that the pointer points into. It is up to the caller to ensure that

`

1182

1180

`/// the returned offset is correct in all terms other than alignment.

`

1183

1181

`///

`

``

1182

`+

/// When this is called during compile-time evaluation (which is unstable), the implementation

`

``

1183

`` +

/// may return usize::MAX in cases where that can never happen at runtime. This is because the

``

``

1184

`+

/// actual alignment of pointers is not known yet during compile-time, so an offset with

`

``

1185

`` +

/// guaranteed alignment can sometimes not be computed. For example, a buffer declared as `[u8;

``

``

1186

`` +

/// N]` might be allocated at an odd or an even address, but at compile-time this is not yet

``

``

1187

`+

/// known, so the execution has to be correct for either choice. It is therefore impossible to

`

``

1188

`+

/// find an offset that is guaranteed to be 2-aligned. (This behavior is subject to change, as usual

`

``

1189

`+

/// for unstable APIs.)

`

``

1190

`+

///

`

1184

1191

`/// # Panics

`

1185

1192

`///

`

1186

1193

`` /// The function panics if align is not a power-of-two.

``