File tree Expand file tree Collapse file tree 1 file changed +12
-3
lines changed Expand file tree Collapse file tree 1 file changed +12
-3
lines changed Original file line number Diff line number Diff line change @@ -2426,15 +2426,20 @@ impl<T> [T] {
2426
2426
where
2427
2427
F : FnMut ( & ' a T ) -> Ordering ,
2428
2428
{
2429
+ // INVARIANTS:
2430
+ // - 0 <= left <= left + size = right <= self.len()
2431
+ // - f returns Less for everything in self[..left]
2432
+ // - f returns Greater for everything in self[right..]
2429
2433
let mut size = self . len ( ) ;
2430
2434
let mut left = 0 ;
2431
2435
let mut right = size;
2432
2436
while left < right {
2433
2437
let mid = left + size / 2 ;
2434
2438
2435
- // SAFETY: the call is made safe by the following invariants:
2436
- // - `mid >= 0`
2437
- // - `mid < size`: `mid` is limited by `[left; right)` bound.
2439
+ // SAFETY: the while condition means `size` is strictly positive, so
2440
+ // `size/2 < size`. Thus `left + size/2 < left + size`, which
2441
+ // coupled with the `left + size <= self.len()` invariant means
2442
+ // we have `left + size/2 < self.len()`, and this is in-bounds.
2438
2443
let cmp = f ( unsafe { self . get_unchecked ( mid) } ) ;
2439
2444
2440
2445
// The reason why we use if/else control flow rather than match
@@ -2452,6 +2457,10 @@ impl<T> [T] {
2452
2457
2453
2458
size = right - left;
2454
2459
}
2460
+
2461
+ // SAFETY: directly true from the overall invariant.
2462
+ // Note that this is `<=`, unlike the assume in the `Ok` path.
2463
+ unsafe { crate :: intrinsics:: assume ( left <= self . len ( ) ) } ;
2455
2464
Err ( left)
2456
2465
}
2457
2466
You can’t perform that action at this time.
0 commit comments