File tree 1 file changed +4
-4
lines changed
1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -1029,11 +1029,11 @@ impl<T: ?Sized> *const T {
1029
1029
#[ cfg_attr( miri, track_caller) ] // even without panics, this helps for Miri backtraces
1030
1030
#[ requires(
1031
1031
// If count is zero, any pointer is valid including null pointer.
1032
- ( count == 0 ) ||
1032
+ ( count == 0 ) ||
1033
1033
// Else if count is not zero, then ensure that adding `count` doesn't cause
1034
1034
// overflow and that both pointers `self` and the result are in the same
1035
1035
// allocation
1036
- ( ( self . addr( ) as isize ) . checked_add( count as isize ) . is_some( ) &&
1036
+ ( ( self . addr( ) as isize ) . checked_add( count as isize ) . is_some( ) &&
1037
1037
kani:: mem:: same_allocation( self , self . wrapping_byte_add( count) ) )
1038
1038
) ]
1039
1039
#[ ensures( |& result|
@@ -1173,11 +1173,11 @@ impl<T: ?Sized> *const T {
1173
1173
#[ cfg_attr( miri, track_caller) ] // even without panics, this helps for Miri backtraces
1174
1174
#[ requires(
1175
1175
// If count is zero, any pointer is valid including null pointer.
1176
- ( count == 0 ) ||
1176
+ ( count == 0 ) ||
1177
1177
// Else if count is not zero, then ensure that subtracting `count` doesn't
1178
1178
// cause overflow and that both pointers `self` and the result are in the
1179
1179
// same allocation
1180
- ( ( self . addr( ) as isize ) . checked_sub( count as isize ) . is_some( ) &&
1180
+ ( ( self . addr( ) as isize ) . checked_sub( count as isize ) . is_some( ) &&
1181
1181
kani:: mem:: same_allocation( self , self . wrapping_byte_sub( count) ) )
1182
1182
) ]
1183
1183
#[ ensures( |& result|
You can’t perform that action at this time.
0 commit comments