Skip to content

Commit 14a278f

Browse files
committed
fix Flux check error
1 parent 76db0b6 commit 14a278f

1 file changed

Lines changed: 18 additions & 6 deletions

File tree

library/core/src/slice/mod.rs

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3021,20 +3021,26 @@ impl<T> [T] {
30213021
#[cfg(not(kani))]
30223022
let half = size / 2;
30233023
#[cfg(kani)]
3024-
half = size / 2;
3024+
{
3025+
half = size / 2;
3026+
}
30253027

30263028
#[cfg(not(kani))]
30273029
let mid = base + half;
30283030
#[cfg(kani)]
3029-
mid = base + half;
3031+
{
3032+
mid = base + half;
3033+
}
30303034

30313035
// SAFETY: the call is made safe by the following invariants:
30323036
// - `mid >= 0`: by definition
30333037
// - `mid < size`: `mid = size / 2 + size / 4 + size / 8 ...`
30343038
#[cfg(not(kani))]
30353039
let cmp = f(unsafe { self.get_unchecked(mid) });
30363040
#[cfg(kani)]
3037-
cmp = f(unsafe { self.get_unchecked(mid) });
3041+
{
3042+
cmp = f(unsafe { self.get_unchecked(mid) });
3043+
}
30383044

30393045
// Binary search interacts poorly with branch prediction, so force
30403046
// the compiler to use conditional moves if supported by the target
@@ -3662,18 +3668,24 @@ impl<T> [T] {
36623668
#[cfg(not(kani))]
36633669
let ptr_read = ptr.add(next_read);
36643670
#[cfg(kani)]
3665-
ptr_read = ptr.add(next_read);
3671+
{
3672+
ptr_read = ptr.add(next_read);
3673+
}
36663674

36673675
#[cfg(not(kani))]
36683676
let prev_ptr_write = ptr.add(next_write - 1);
36693677
#[cfg(kani)]
3670-
prev_ptr_write = ptr.add(next_write - 1);
3678+
{
3679+
prev_ptr_write = ptr.add(next_write - 1);
3680+
}
36713681
if !same_bucket(&mut *ptr_read, &mut *prev_ptr_write) {
36723682
if next_read != next_write {
36733683
#[cfg(not(kani))]
36743684
let ptr_write = prev_ptr_write.add(1);
36753685
#[cfg(kani)]
3676-
ptr_write = prev_ptr_write.add(1);
3686+
{
3687+
ptr_write = prev_ptr_write.add(1);
3688+
}
36773689
mem::swap(&mut *ptr_read, &mut *ptr_write);
36783690
}
36793691
next_write += 1;

0 commit comments

Comments
 (0)