From c4b9c199c24c24a0ccb5093e69a47bb5d20337c5 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 19:18:45 -0700
Subject: [PATCH] Apply suggestions from code review

Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
---
 library/contracts/safety/build.rs |  2 +-
 library/core/src/ptr/mod.rs       |  1 -
 library/core/src/ub_checks.rs     | 12 +++++++-----
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/library/contracts/safety/build.rs b/library/contracts/safety/build.rs
index 32258fb328eec..e74a4c9e57d6e 100644
--- a/library/contracts/safety/build.rs
+++ b/library/contracts/safety/build.rs
@@ -1,4 +1,4 @@
 fn main() {
     // We add the configurations here to be checked.
     println!("cargo:rustc-check-cfg=cfg(kani_host)");
-}
\ No newline at end of file
+}
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index a6706c389752d..61d101c766f49 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -1769,7 +1769,6 @@ pub unsafe fn read_volatile<T>(src: *const T) -> T {
 #[stable(feature = "volatile", since = "1.9.0")]
 #[rustc_diagnostic_item = "ptr_write_volatile"]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-// What happens to the value that was replaced? No drop?
 #[safety::requires(ub_checks::can_write(dst))]
 pub unsafe fn write_volatile<T>(dst: *mut T, src: T) {
     // SAFETY: the caller must uphold the safety contract for `volatile_store`.
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index a6e890023bfeb..b864b63c5c661 100644
--- a/library/core/src/ub_checks.rs
+++ b/library/core/src/ub_checks.rs
@@ -168,11 +168,12 @@ pub use predicates::*;
 /// At runtime, they are no-op, and always return true.
 #[cfg(not(kani))]
 mod predicates {
-    /// Check if a pointer can be dereferenced. I.e.:
-    ///   * `src` must be valid for reads. See [crate::ptr] documentation.
-    ///   * `src` must be properly aligned. Use read_unaligned if this is not the case.
-    ///   * `src` must point to a properly initialized value of type T.
+    /// Checks if a pointer can be dereferenced, ensuring:
+    ///   * `src` is valid for reads (see [`crate::ptr`] documentation).
+    ///   * `src` is properly aligned (use `read_unaligned` if not).
+    ///   * `src` points to a properly initialized value of type `T`.
     ///
+    /// [`crate::ptr`]: https://doc.rust-lang.org/std/ptr/index.html
     pub fn can_dereference<T>(src: *const T) -> bool {
         let _ = src;
         true
@@ -180,7 +181,7 @@ mod predicates {
 
     /// Check if a pointer can be written to:
     /// * `dst` must be valid for writes.
-    /// * `dst` must be properly aligned. Use [`write_unaligned`] if this is not the
+    /// * `dst` must be properly aligned. Use `write_unaligned` if this is not the
     ///    case.
     pub fn can_write<T>(dst: *mut T) -> bool {
         let _ = dst;
@@ -195,6 +196,7 @@ mod predicates {
         true
     }
 
+    /// Check if a pointer can be the target of unaligned writes.
     /// * `dst` must be valid for writes.
     pub fn can_write_unaligned<T>(dst: *mut T) -> bool {
         let _ = dst;