From 4b925fd3a412b945ec0df8d5f7b8406c37c6a6b9 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Thu, 9 Mar 2023 15:35:42 -0500
Subject: [PATCH] Avoid undefined behavior in AnySlice::new() (#2288)

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 library/kani/src/slice.rs      |  2 +-
 tests/kani/Slice/slice-drop.rs | 25 +++++++++++++++++++++++++
 2 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 tests/kani/Slice/slice-drop.rs

diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
index 0f3fea16b3a4..f06118a4b2f5 100644
--- a/library/kani/src/slice.rs
+++ b/library/kani/src/slice.rs
@@ -71,7 +71,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
             //         *(ptr as *mut T).add(i) = any();
             //     }
             while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
-                *any_slice.ptr.add(i) = any();
+                std::ptr::write(any_slice.ptr.add(i), any());
                 i += 1;
             }
         }
diff --git a/tests/kani/Slice/slice-drop.rs b/tests/kani/Slice/slice-drop.rs
new file mode 100644
index 000000000000..41d596c3be46
--- /dev/null
+++ b/tests/kani/Slice/slice-drop.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Assigning to a memory location via pointer dereferencing causes Drop::drop to be called for the location to which the pointer points.
+// Here, kani::Arbitrary implementation for MyStruct deterministically sets MyStruct.0 to 1.
+// We check whether AnySlice will properly initialize memory making the assertion in drop() to pass.
+
+struct MyStruct(i32);
+
+impl Drop for MyStruct {
+    fn drop(&mut self) {
+        assert!(self.0 == 1);
+    }
+}
+
+impl kani::Arbitrary for MyStruct {
+    fn any() -> Self {
+        MyStruct(1)
+    }
+}
+
+#[kani::proof]
+fn my_proof() {
+    let my_slice = kani::slice::any_slice::<MyStruct, 1>();
+}