Document behavior of `checked_size_of_raw` wrt `isize::MAX`

[joshlf]

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.

[rajath-mk]

Thank you for raising this! I have raised a PR adding documentation. Let us know if we can make it more clear or if you see anything else that is missing.