fixup! Fix past mis-merges

Author: tautschnig

library/core/src/alloc/layout.rs

@@ -203,6 +203,8 @@ impl Layout {
     #[rustc_const_stable(feature = "const_alloc_layout", since = "1.85.0")]
     #[must_use]
     #[inline]
+    #[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: ?Sized>(t: &T) -> Self {
         let (size, align) = (size_of_val(t), align_of_val(t));
         // SAFETY: see rationale in `new` for why this is using the unsafe variant

library/core/src/intrinsics/mod.rs

@@ -3322,7 +3322,6 @@ pub fn contract_check_ensures<'a, Ret, C: Fn(&'a Ret) -> bool>(ret: &'a Ret, con
 #[rustc_nounwind]
 #[unstable(feature = "core_intrinsics", issue = "none")]
 #[rustc_intrinsic]
-#[rustc_intrinsic_must_be_overridden]
 // VTable pointers must be valid for dereferencing at least 3 `usize` (size, alignment and drop):
 // <https://github.com/rust-lang/unsafe-code-guidelines/issues/166>
 #[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))]
@@ -3338,7 +3337,6 @@ pub unsafe fn vtable_size(_ptr: *const ()) -> usize {
 #[rustc_nounwind]
 #[unstable(feature = "core_intrinsics", issue = "none")]
 #[rustc_intrinsic]
-#[rustc_intrinsic_must_be_overridden]
 // VTable pointers must be valid for dereferencing at least 3 `usize` (size, alignment and drop):
 // <https://github.com/rust-lang/unsafe-code-guidelines/issues/166>
 #[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))]

library/core/src/ptr/const_ptr.rs

@@ -1,5 +1,3 @@
-use core::mem;
-
 use safety::{ensures, requires};
 
 use super::*;

library/core/src/ptr/mut_ptr.rs

@@ -1,5 +1,3 @@
-use core::mem;
-
 use safety::{ensures, requires};
 
 use super::*;

library/core/src/ptr/non_null.rs

@@ -2217,7 +2217,7 @@ mod verify {
         use core::mem::MaybeUninit;
 
         const SIZE: usize = 100000;
-        let arr: [MaybeUninit<i32>; SIZE] = MaybeUninit::uninit_array();
+        let arr = [MaybeUninit::uninit(); SIZE];
         let slice: &[MaybeUninit<i32>] = kani::slice::any_slice_of_array(&arr);
         let ptr = NonNull::slice_from_raw_parts(
             NonNull::new(slice.as_ptr() as *mut MaybeUninit<i32>).unwrap(),
@@ -2234,7 +2234,7 @@ mod verify {
         use core::mem::MaybeUninit;
 
         const SIZE: usize = 100000;
-        let mut arr: [MaybeUninit<i32>; SIZE] = MaybeUninit::uninit_array();
+        let mut arr = [MaybeUninit::uninit(); SIZE];
         let slice: &[MaybeUninit<i32>] = kani::slice::any_slice_of_array(&mut arr);
         let ptr = NonNull::slice_from_raw_parts(
             NonNull::new(slice.as_ptr() as *mut MaybeUninit<i32>).unwrap(),
@@ -2479,7 +2479,7 @@ mod verify {
         }
     }
 
-    #[kani::proof_for_contract(NonNull::sub_ptr)]
+    #[kani::proof_for_contract(NonNull::offset_from_unsigned)]
     pub fn non_null_check_sub_ptr() {
         const SIZE: usize = core::mem::size_of::<i32>() * 1000;
         let mut generator1 = kani::PointerGenerator::<SIZE>::new();
@@ -2501,7 +2501,7 @@ mod verify {
         let origin_nonnull = unsafe { NonNull::new(origin).unwrap() };
 
         unsafe {
-            let distance = ptr_nonnull.sub_ptr(origin_nonnull);
+            let distance = ptr_nonnull.offset_from_unsigned(origin_nonnull);
         }
     }