From 44824f175b73d098393f3afbb94dfe0d99f57e0f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 23 Jul 2024 10:49:15 +0000
Subject: [PATCH] Add harness for Alignment::new_unchecked

In #33 a contract was added to `Alignment::new_unchecked`, but its
verification was only implicit through `Layout`, and may be affected by
future changes to the contract that was added to `Layout`. This commit
remedies this by adding a separate harness just for `Alignment`.
---
 library/core/src/ptr/alignment.rs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index e5f5bf6a50313..f4f68c2bb45ee 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -370,3 +370,20 @@ enum AlignmentEnum {
     _Align1Shl62 = 1 << 62,
     _Align1Shl63 = 1 << 63,
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(Alignment::new_unchecked)]
+    pub fn check_new_unchecked() {
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let alignment = Alignment::new_unchecked(a);
+            assert_eq!(alignment.as_usize(), a);
+            assert!(a.is_power_of_two());
+        }
+    }
+}