count cannot overflow isize in preconditions for byte_add and byte_sub

Author: Carolyn Zech

library/backtrace

@@ -1060,7 +1060,8 @@ impl<T: ?Sized> *const T {
         // Else if count is not zero, then ensure that adding `count` doesn't cause 
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
-        ((self.addr() as isize).checked_add(count as isize).is_some() &&
+        (count <= isize::MAX as usize &&
+            (self.addr() as isize).checked_add(count as isize).is_some() &&
             core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
     )]
     #[ensures(|&result|
@@ -1203,7 +1204,7 @@ impl<T: ?Sized> *const T {
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
-        ((self.addr() as isize).checked_sub(count as isize).is_some() &&
+        (count <= isize::MAX as usize && (self.addr() as isize).checked_sub(count as isize).is_some() &&
             core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
     #[ensures(|&result|

library/core/src/ptr/const_ptr.rs

@@ -1157,7 +1157,7 @@ impl<T: ?Sized> *mut T {
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation.
-        ((self.addr() as isize).checked_add(count as isize).is_some() &&
+        (count <= isize::MAX as usize && (self.addr() as isize).checked_add(count as isize).is_some() &&
             core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
     )]
     #[ensures(|&result|
@@ -1303,7 +1303,7 @@ impl<T: ?Sized> *mut T {
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation.
-        ((self.addr() as isize).checked_sub(count as isize).is_some() &&
+        (count <= isize::MAX as usize && (self.addr() as isize).checked_sub(count as isize).is_some() &&
             core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
     #[ensures(|&result|