Syntax fixes

Author: tautschnig

library/core/src/alloc/layout.rs

@@ -124,7 +124,6 @@ impl Layout {
     #[requires(align > 0)]
     #[requires((align & (align - 1)) == 0)]
     #[requires(size <= isize::MAX as usize - (align - 1))]
-    #[rustc_diagnostic_item = "from_size_align_unchecked"]
     pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
         // SAFETY: the caller is required to uphold the preconditions.
         unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -505,19 +504,20 @@ impl fmt::Display for LayoutError {
 #[unstable(feature="kani", issue="none")]
 mod verify {
     use super::*;
-    use crate::kani;
 
-    #[kani::proof_for_contract(from_size_align_unchecked)]
+    #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
     pub fn check_from_size_align_unchecked() {
         let s = kani::any::<usize>();
         let shift_index = kani::any::<u8>();
         let a : usize = 1 << shift_index;
 
         kani::assume(a > 0);
-        // kani::assume(s <= isize::MAX as usize - (a - 1));
+        kani::assume(s <= isize::MAX as usize - (a - 1));
 
-        let layout = from_size_align_unchecked(s, a);
-        assert_eq!(layout.size(), s);
-        assert_eq!(layout.align(), a);
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            assert_eq!(layout.size(), s);
+            assert_eq!(layout.align(), a);
+        }
     }
 }

library/core/src/ptr/alignment.rs

@@ -82,7 +82,6 @@ impl Alignment {
     #[inline]
     #[requires(align > 0)]
     #[requires((align & (align - 1)) == 0)]
-    #[rustc_diagnostic_item = "new_unchecked"]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(