Clarify is_inbounds docs (#3974)

See
#3956 (comment)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

library/kani_core/src/mem.rs

@@ -168,15 +168,13 @@ 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 return `false` if `ptr` is null
+        /// or the size of the val pointed to exceeds `isize::MAX`.
+        /// Otherwise, it will return `true` if and only if `ptr` points to allocated memory
+        /// that can hold data of size calculated from `T`.
+        /// Note that Kani does not support reasoning about pointers to unallocated memory,
+        /// so if `ptr` does not point to allocated memory, verification will fail.
         #[crate::kani::unstable_feature(
             feature = "mem-predicates",
             issue = 3946,
@@ -192,7 +190,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(