clarify is_inbounds docs

Author: carolynzech

library/kani_core/src/mem.rs

@@ -168,15 +168,14 @@ macro_rules! kani_mem {
 
         /// Checks that `ptr` points to an allocation that can hold data of size calculated from `T`.
         ///
-        /// This will panic if `ptr` points to an invalid `non_null`
-        /// Returns `false` if:
-        /// - The computed size overflows.
-        /// - The computed size exceeds `isize::MAX`.
-        /// - The pointer is null (except for zero-sized types).
-        /// - The pointer references unallocated memory.
-        ///
-        /// This function aligns with Rust's memory safety requirements, which restrict valid allocations
-        /// to sizes no larger than `isize::MAX`.
+        /// This function always returns `true` for ZSTs, since every pointer to a ZST is valid.
+        /// For non-ZSTs, this function will:
+        ///  - Panic if `ptr` does not point to allocated memory,
+        ///  - Return `false` if the size of the val pointed to exceeds `isize::MAX`,
+        ///  - Return `false` if the pointer is null.
+        ///  
+        /// If none of the above conditions hold, it will return `true` if and only if 
+        /// `ptr` points to allocated memory that can hold data of size calculated from `T`.
         #[crate::kani::unstable_feature(
             feature = "mem-predicates",
             issue = 3946,
@@ -192,7 +191,7 @@ macro_rules! kani_mem {
             } else {
                 // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be
                 // stubbed.
-                // We first assert that the data_ptr
+                // We first assert that the data_ptr points to a valid allocation.
                 let data_ptr = ptr as *const ();
                 if !unsafe { is_allocated(data_ptr, 0) } {
                     crate::kani::unsupported(