From 1246d25de187fd0d84a23cc49ab147d01b4028ab Mon Sep 17 00:00:00 2001
From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com>
Date: Wed, 4 Dec 2024 15:25:23 -0800
Subject: [PATCH] same_allocation offset

---
 library/core/src/ptr/non_null.rs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index c8ef5334356b4..a3d9e2b0351b9 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -511,7 +511,7 @@ impl<T: ?Sized> NonNull<T> {
     #[requires(
         count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
        (self.as_ptr() as isize).checked_add(count.wrapping_mul(core::mem::size_of::<T>() as isize)).is_some() &&
-        kani::mem::same_allocation(self.as_ptr() as *const (), self.as_ptr().wrapping_offset(count) as *const ())
+        (count == 0 || kani::mem::same_allocation(self.as_ptr() as *const (), self.as_ptr().wrapping_offset(count) as *const ()))
     )]
     #[ensures(|result: &Self| result.as_ptr() == self.as_ptr().wrapping_offset(count))]
     pub const unsafe fn offset(self, count: isize) -> Self
@@ -2424,7 +2424,7 @@ mod verify {
 
     #[kani::proof_for_contract(NonNull::byte_sub)]
     pub fn non_null_check_byte_sub() {
-        const SIZE: usize = mem::size_of::<i32>() * 100;
+        const SIZE: usize = mem::size_of::<i32>() * 10000;
         let mut generator = PointerGenerator::<SIZE>::new();
         let count: usize = kani::any();
         let raw_ptr: *mut i32 = generator.any_in_bounds().ptr as *mut i32;
@@ -2436,7 +2436,7 @@ mod verify {
 
     #[kani::proof_for_contract(NonNull::offset)]
     pub fn non_null_check_offset() {
-        const SIZE: usize = mem::size_of::<i32>() * 100;
+        const SIZE: usize = mem::size_of::<i32>() * 10000;
         let mut generator = PointerGenerator::<SIZE>::new();
         let start_ptr = generator.any_in_bounds().ptr as *mut i32;
         let ptr_nonnull = NonNull::new(start_ptr).unwrap();
@@ -2448,7 +2448,7 @@ mod verify {
 
     #[kani::proof_for_contract(NonNull::map_addr)]
     pub fn non_null_check_map_addr() {
-        const SIZE: usize = 100;
+        const SIZE: usize = 10000;
         let arr: [i32; SIZE] = kani::any();
         let ptr = NonNull::new(arr.as_ptr() as *mut i32).unwrap();
         let new_offset: usize = kani::any_where(|&x| x <= SIZE);
@@ -2460,7 +2460,7 @@ mod verify {
 
     #[kani::proof_for_contract(NonNull::with_addr)]
     pub fn non_null_check_with_addr() {
-        const SIZE: usize = 100;
+        const SIZE: usize = 10000;
         let arr: [i32; SIZE] = kani::any();
         let ptr = NonNull::new(arr.as_ptr() as *mut i32).unwrap();
         let new_offset: usize = kani::any_where(|&x| x <= SIZE);