update contracts

Author: danielhumanmod

library/core/src/ptr/non_null.rs

@@ -502,7 +502,10 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
-    #[kani::requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()))]
+    #[kani::requires(
+        count <= isize::MAX &&
+        kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const())
+    )]
     #[kani::ensures(|result: &Self| result.as_ptr() == self.as_ptr().byte_offset(count))]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has
@@ -581,10 +584,10 @@ impl<T: ?Sized> NonNull<T> {
     #[rustc_allow_const_fn_unstable(set_ptr_value)]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
-    #[kani::requires(kani::mem::same_allocation(
-        self.as_ptr() as *const(),
-        ((self.as_ptr() as *const () as usize) + count) as *const()
-    ))]
+    #[kani::requires(
+        count <= usize::MAX &&
+        kani::mem::same_allocation(self.as_ptr() as *const(), (self.as_ptr().byte_add(count)) as *const())
+    )]
     #[kani::ensures(
         |result: &NonNull<T>|
         (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count)
@@ -1829,9 +1832,6 @@ mod verify {
         let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() };
         let count: usize = kani::any();
 
-        kani::assume(count.checked_mul(mem::size_of::<i32>()).is_some());
-        kani::assume(count * mem::size_of::<i32>() <= (isize::MAX as usize));
-
         unsafe {
             let result = ptr.byte_add(count);
         }
@@ -1846,8 +1846,6 @@ mod verify {
         let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() };
         let count: isize = kani::any();
 
-        kani::assume(count.checked_mul(mem::size_of::<i32>() as isize).is_some());
-        kani::assume(count * (mem::size_of::<i32>() as isize) <= (isize::MAX as isize));
         unsafe {
             let result = ptr.byte_offset(count);
         }