Apply suggestions from code review

Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

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)");
-}
+}

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`.

library/core/src/ub_checks.rs

@@ -168,19 +168,20 @@ 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
     }
 
     /// 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;