Skip to content

Commit a0a60ab

Browse files
jrey8343claude
andcommitted
Fix borrow checker errors in Kani _mut harnesses
Capture slice.len() before mutable method calls to avoid "cannot borrow *slice as immutable" errors in: - check_first_chunk_mut - check_as_flattened_mut Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 1f0cd53 commit a0a60ab

1 file changed

Lines changed: 4 additions & 2 deletions

File tree

library/core/src/slice/mod.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5543,8 +5543,9 @@ mod verify {
55435543
const ARR_SIZE: usize = 64;
55445544
let mut arr: [u8; ARR_SIZE] = kani::any();
55455545
let slice = kani::slice::any_slice_of_array_mut(&mut arr);
5546+
let len = slice.len();
55465547
let result = slice.first_chunk_mut::<$N>();
5547-
if slice.len() >= $N {
5548+
if len >= $N {
55485549
assert!(result.is_some());
55495550
} else {
55505551
assert!(result.is_none());
@@ -5769,8 +5770,9 @@ mod verify {
57695770
const ARR_SIZE: usize = 16;
57705771
let mut arr: [[u8; $N]; ARR_SIZE] = kani::any();
57715772
let slice: &mut [[u8; $N]] = kani::slice::any_slice_of_array_mut(&mut arr);
5773+
let len = slice.len();
57725774
let flat = slice.as_flattened_mut();
5773-
assert!(flat.len() == slice.len() * $N);
5775+
assert!(flat.len() == len * $N);
57745776
}
57755777
};
57765778
}

0 commit comments

Comments
 (0)