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] {
24262426 where
24272427 F : FnMut ( & ' a T ) -> Ordering ,
24282428 {
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..]
24292433 let mut size = self . len ( ) ;
24302434 let mut left = 0 ;
24312435 let mut right = size;
24322436 while left < right {
24332437 let mid = left + size / 2 ;
24342438
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.
24382443 let cmp = f ( unsafe { self . get_unchecked ( mid) } ) ;
24392444
24402445 // The reason why we use if/else control flow rather than match
@@ -2452,6 +2457,10 @@ impl<T> [T] {
24522457
24532458 size = right - left;
24542459 }
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 ( ) ) } ;
24552464 Err ( left)
24562465 }
24572466
You can’t perform that action at this time.
0 commit comments