Add harnesses for all functions in Alignment

library/core/src/ptr/alignment.rs

@@ -80,8 +80,7 @@ impl Alignment {
  #[unstable(feature = "ptr_alignment_type", issue = "102070")]
  #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
  #[inline]
- #[requires(align > 0)]
- #[requires((align & (align - 1)) == 0)]
+ #[requires(align > 0 && (align & (align - 1)) == 0)]
  pub const unsafe fn new_unchecked(align: usize) -> Self {
  #[cfg(debug_assertions)]
  assert_unsafe_precondition!(
@@ -370,3 +369,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());
+ }
+ }
+}