Skip to content

Commit c8b15c6

Browse files
authored
Make is_inbounds public (#3958)
Resolves #3946 This PR makes `kani::mem::is_inbounds` publicly accessible, allowing direct validation of pointer sizes By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 641756b commit c8b15c6

File tree

3 files changed

+17
-2
lines changed

3 files changed

+17
-2
lines changed

library/kani_core/src/mem.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -177,7 +177,12 @@ macro_rules! kani_mem {
177177
///
178178
/// This function aligns with Rust's memory safety requirements, which restrict valid allocations
179179
/// to sizes no larger than `isize::MAX`.
180-
fn is_inbounds<T: ?Sized>(ptr: *const T) -> bool {
180+
#[crate::kani::unstable_feature(
181+
feature = "mem-predicates",
182+
issue = 3946,
183+
reason = "experimental memory predicate API"
184+
)]
185+
pub fn is_inbounds<T: ?Sized>(ptr: *const T) -> bool {
181186
// If size overflows, then pointer cannot be inbounds.
182187
let Some(sz) = checked_size_of_raw(ptr) else { return false };
183188
if sz == 0 {
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
Complete - 1 successfully verified harnesses, 0 failures, 1 total.
1+
Complete - 2 successfully verified harnesses, 0 failures, 2 total.

tests/expected/MemPredicates/ptr_size_validity.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,16 @@ extern crate kani;
88
mod size {
99
use super::*;
1010

11+
#[kani::proof]
12+
fn verify_is_inbounds() {
13+
let val = 42u8;
14+
let ptr = &val as *const u8;
15+
assert!(kani::mem::is_inbounds(ptr));
16+
17+
let null_ptr: *const u8 = core::ptr::null();
18+
assert!(!kani::mem::is_inbounds(null_ptr));
19+
}
20+
1121
#[kani::proof]
1222
fn verify_checked_size_of_raw_exceeds_isize_max() {
1323
let len_exceeding_isize_max = (isize::MAX as usize) + 1;

0 commit comments

Comments
 (0)