Skip to content

Commit aca1c9e

Browse files
committed
Address PR feedback
- Improve first / last logic - Add comment to invariant - Fix IterMut invariant
1 parent 4de4a2e commit aca1c9e

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

library/core/src/slice/iter.rs

+5-4
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,7 @@ impl<T> Invariant for Iter<'_, T> {
171171
/// `self.ptr` and `self.end_or_len`.
172172
fn is_safe(&self) -> bool {
173173
let ty_size = crate::mem::size_of::<T>();
174+
// Use `abs_diff` since `end_or_len` may be smaller than `ptr` if `T` is a ZST.
174175
let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
175176
if ty_size == 0 || distance == 0 {
176177
self.ptr.is_aligned()
@@ -236,8 +237,8 @@ impl<T> Invariant for IterMut<'_, T> {
236237
if ty_size == 0 || distance == 0 {
237238
self.ptr.is_aligned()
238239
} else {
239-
let slice_ptr: *const [T] =
240-
crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
240+
let slice_ptr: *mut [T] =
241+
crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / ty_size);
241242
crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
242243
&& self.ptr.addr().get() <= self.end_or_len as usize
243244
&& distance % ty_size == 0
@@ -3525,8 +3526,8 @@ mod verify {
35253526

35263527
fn any_slice<T>(orig_slice: &[T]) -> &[T] {
35273528
if kani::any() {
3528-
let first = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
3529-
let last = kani::any_where(|idx: &usize| *idx >= first && *idx <= orig_slice.len());
3529+
let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
3530+
let first = kani::any_where(|idx: &usize| *idx <= last);
35303531
&orig_slice[first..last]
35313532
} else {
35323533
let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;

0 commit comments

Comments
 (0)