Use autoharness for several Alignment functions

Author: tautschnig

.github/workflows/kani.yml

@@ -80,11 +80,18 @@ jobs:
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern ptr::align_offset::mod_inv \
+            --include-pattern ptr::alignment::Alignment::as_nonzero \
+            --include-pattern ptr::alignment::Alignment::as_usize \
+            --include-pattern ptr::alignment::Alignment::log2 \
+            --include-pattern ptr::alignment::Alignment::mask \
+            --include-pattern ptr::alignment::Alignment::new \
+            --include-pattern ptr::alignment::Alignment::new_unchecked \
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \
             --include-pattern time::Duration::from_secs \
             --exclude-pattern time::Duration::from_secs_f \
+            --exclude-pattern ::precondition_check \
             --harness-timeout 5m \
             --default-unwind 1000 \
             --jobs=3 --output-format=terse

library/core/src/ptr/alignment.rs

@@ -410,50 +410,4 @@ mod verify {
     // pub fn check_of_i32() {
     //     let _ = Alignment::of::<i32>();
     // }
-
-    // pub const fn new(align: usize) -> Option<Self>
-    #[kani::proof_for_contract(Alignment::new)]
-    pub fn check_new() {
-        let a = kani::any::<usize>();
-        let _ = Alignment::new(a);
-    }
-
-    // pub const unsafe fn new_unchecked(align: usize) -> Self
-    #[kani::proof_for_contract(Alignment::new_unchecked)]
-    pub fn check_new_unchecked() {
-        let a = kani::any::<usize>();
-        unsafe {
-            let _ = Alignment::new_unchecked(a);
-        }
-    }
-
-    // pub const fn as_usize(self) -> usize
-    #[kani::proof_for_contract(Alignment::as_usize)]
-    pub fn check_as_usize() {
-        let a = kani::any::<usize>();
-        if let Some(alignment) = Alignment::new(a) {
-            assert_eq!(alignment.as_usize(), a);
-        }
-    }
-
-    // pub const fn as_nonzero(self) -> NonZero<usize>
-    #[kani::proof_for_contract(Alignment::as_nonzero)]
-    pub fn check_as_nonzero() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.as_nonzero();
-    }
-
-    // pub const fn log2(self) -> u32
-    #[kani::proof_for_contract(Alignment::log2)]
-    pub fn check_log2() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.log2();
-    }
-
-    // pub const fn mask(self) -> usize
-    #[kani::proof_for_contract(Alignment::mask)]
-    pub fn check_mask() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.mask();
-    }
 }