From e88052089dfb19c9779c72173b9913b63a62170b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 17 Oct 2024 15:51:32 +0000
Subject: [PATCH] Fix contract (incomplete)

---
 library/alloc/src/boxed/thin.rs | 4 +++-
 library/alloc/src/lib.rs        | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs
index 69aa551420fb5..40d0b12d53624 100644
--- a/library/alloc/src/boxed/thin.rs
+++ b/library/alloc/src/boxed/thin.rs
@@ -6,6 +6,7 @@ use safety::requires;
 #[cfg(kani)]
 #[unstable(feature="kani", issue="none")]
 use core::kani;
+use core::ub_checks;
 
 use core::error::Error;
 use core::fmt::{self, Debug, Display, Formatter};
@@ -366,9 +367,10 @@ impl<H> WithHeader<H> {
     }
 
     // Safety:
-    #[requires(value.is_null() || value.is_aligned())]
     // - Assumes that either `value` can be dereferenced, or is the
     //   `NonNull::dangling()` we use when both `T` and `H` are ZSTs.
+    #[requires((mem::size_of_val_raw(value) == 0 && size_of::<H>() == 0) ||
+        ub_checks::can_dereference(value))]
     unsafe fn drop<T: ?Sized>(&self, value: *mut T) {
         struct DropGuard<H> {
             ptr: NonNull<u8>,
diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs
index d28c5a29df2b9..663524fedc176 100644
--- a/library/alloc/src/lib.rs
+++ b/library/alloc/src/lib.rs
@@ -92,6 +92,7 @@
 // Library features:
 // tidy-alphabetical-start
 #![cfg_attr(kani, feature(kani))]
+#![cfg_attr(kani, feature(ub_checks))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
 #![feature(alloc_layout_extra)]