Skip to content

Commit fc64164

Browse files
authored
Put loop_modifies in cfg_attr(kani)
1 parent 05bc9fe commit fc64164

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

library/core/src/slice/mod.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1012,7 +1012,12 @@ impl<T> [T] {
10121012

10131013
let mut i = 0;
10141014
#[safety::loop_invariant(i <= n)]
1015-
#[kani::loop_modifies(unsafe {slice::from_raw_parts_mut(a.as_mut_ptr(), n)}, unsafe {slice::from_raw_parts_mut(b.as_mut_ptr(), n)}, &i)]
1015+
#[cfg_attr(kani,
1016+
kani::loop_modifies(
1017+
unsafe {slice::from_raw_parts_mut(a.as_mut_ptr(), n)},
1018+
unsafe {slice::from_raw_parts_mut(b.as_mut_ptr(), n)},
1019+
&i)
1020+
)]
10161021
while i < n {
10171022
mem::swap(&mut a[i], &mut b[n - 1 - i]);
10181023
i += 1;

0 commit comments

Comments
 (0)