Make is_inbounds public

library/kani_core/src/mem.rs

@@ -177,7 +177,12 @@ macro_rules! kani_mem {
         ///
         /// This function aligns with Rust's memory safety requirements, which restrict valid allocations
         /// to sizes no larger than `isize::MAX`.
-        fn is_inbounds<T: ?Sized>(ptr: *const T) -> bool {
+        #[crate::kani::unstable_feature(
+            feature = "mem-predicates",
+            issue = 3946,
+            reason = "experimental memory predicate API"
+        )]
+        pub fn is_inbounds<T: ?Sized>(ptr: *const T) -> bool {
             // If size overflows, then pointer cannot be inbounds.
             let Some(sz) = checked_size_of_raw(ptr) else { return false };
             if sz == 0 {

tests/expected/MemPredicates/ptr_size_validity.expected

@@ -1 +1 @@
-Complete - 1 successfully verified harnesses, 0 failures, 1 total.
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.

tests/expected/MemPredicates/ptr_size_validity.rs

@@ -8,6 +8,16 @@ extern crate kani;
 mod size {
     use super::*;
 
+    #[kani::proof]
+    fn verify_is_inbounds() {
+        let val = 42u8;
+        let ptr = &val as *const u8;
+        assert!(kani::mem::is_inbounds(ptr));
+
+        let null_ptr: *const u8 = core::ptr::null();
+        assert!(!kani::mem::is_inbounds(null_ptr));
+    }
+
     #[kani::proof]
     fn verify_checked_size_of_raw_exceeds_isize_max() {
         let len_exceeding_isize_max = (isize::MAX as usize) + 1;