Auto merge of #127777 - matthiaskrgr:rollup-qp2vkan, r=matthiaskrgr · model-checking/verify-rust-std@a778c83 (original) (raw)

`@@ -735,9 +735,9 @@ impl<T: ?Sized> NonNull {

735

`///

736

`` /// * self and origin must either

737

`///

738

/// * point to the same address, or

738

739

`/// * both be derived from a pointer to the same [allocated object], and the memory range between

739

/// the two pointers must be either empty or in bounds of that object. (See below for an example.)

740

/// * or both be derived from an integer literal/constant, and point to the same address.

740

/// the two pointers must be in bounds of that object. (See below for an example.)

741

`///

742

`/// * The distance between the pointers, in bytes, must be an exact multiple

743

`` /// of the size of T.

`@@ -789,14 +789,15 @@ impl<T: ?Sized> NonNull {

789

`/// let ptr1 = NonNull::new(Box::into_raw(Box::new(0u8))).unwrap();

790

`/// let ptr2 = NonNull::new(Box::into_raw(Box::new(1u8))).unwrap();

791

`/// let diff = (ptr2.addr().get() as isize).wrapping_sub(ptr1.addr().get() as isize);

792

/// // Make ptr2_other an "alias" of ptr2, but derived from ptr1.

793

/// let ptr2_other = NonNull::new(ptr1.as_ptr().wrapping_byte_offset(diff)).unwrap();

792

/// // Make ptr2_other an "alias" of ptr2.add(1), but derived from ptr1.

793

/// let diff_plus_1 = diff.wrapping_add(1);

794

/// let ptr2_other = NonNull::new(ptr1.as_ptr().wrapping_byte_offset(diff_plus_1)).unwrap();

794

795

`/// assert_eq!(ptr2.addr(), ptr2_other.addr());

795

796

`/// // Since ptr2_other and ptr2 are derived from pointers to different objects,

796

797

`/// // computing their offset is undefined behavior, even though

797

/// // they point to the same address!

798

/// // they point to addresses that are in-bounds of the same object!

798

799

`///

799

/// let zero = unsafe { ptr2_other.offset_from(ptr2) }; // Undefined Behavior

800

/// let one = unsafe { ptr2_other.offset_from(ptr2) }; // Undefined Behavior! ⚠️

800

801

```` /// ```

````

801

802

`#[inline]

802

803

`#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces