generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 129
Closed
Labels
T-UserTag user issues / requestsTag user issues / requests[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.
Description
kani/library/kani_core/src/mem.rs
Lines 130 to 135 in 707309b
| /// Compute the size of the val pointed to if it is safe to do so. | |
| /// | |
| /// Return `None` if an overflow would occur, or if alignment is not power of two. | |
| /// TODO: Optimize this if T is sized. | |
| #[kanitool::fn_marker = "CheckedSizeOfIntrinsic"] | |
| pub fn checked_size_of_raw<T: ?Sized>(ptr: *const T) -> Option<usize> { |
Does checked_size_of_raw return None for sizes larger than isize::MAX? All Rust allocations are no more than isize::MAX bytes long, and many unsafe stdlib APIs require pointer referents to be no more than isize::MAX as a safety precondition. It'd be good to document the behavior one way or the other.
Same for its callers - is_inbounds and the callers of is_inbounds.
Metadata
Metadata
Assignees
Labels
T-UserTag user issues / requestsTag user issues / requests[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.