Skip to content

Commit a8e23b3

Browse files
committed
Update char contracts
1 parent 171d1ab commit a8e23b3

File tree

1 file changed

+13
-2
lines changed

1 file changed

+13
-2
lines changed

library/core/src/iter/range.rs

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,7 @@ macro_rules! step_unsigned_methods {
212212
unsafe { start.unchecked_add(n as Self) }
213213
}
214214

215-
#[requires(start.checked_sub(n as Self).is_some())]
215+
#[requires(start >= n)]
216216
#[inline]
217217
unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
218218
// SAFETY: the caller has to guarantee that `start - n` doesn't overflow.
@@ -503,6 +503,12 @@ impl Step for char {
503503
}
504504

505505
#[requires((start as u32).checked_add(count as u32).is_some())]
506+
#[requires({
507+
let dist = (start as u32).checked_add(count as u32);
508+
dist.is_some() &&
509+
(start >= 0xD800 || dist.unwrap() < 0xD800 ||
510+
dist.unwrap().checked_add(0x800).is_some())
511+
})]
506512
#[inline]
507513
unsafe fn forward_unchecked(start: char, count: usize) -> char {
508514
let start = start as u32;
@@ -519,7 +525,12 @@ impl Step for char {
519525
unsafe { char::from_u32_unchecked(res) }
520526
}
521527

522-
#[requires((start as u32).checked_sub(count as u32).is_some())]
528+
#[requires({
529+
let dist = (start as u32).checked_sub(count as u32);
530+
dist.is_some() &&
531+
(start < 0xE000 || dist.unwrap() >= 0xE000 ||
532+
dist.unwrap().checked_sub(0x800).is_some())
533+
})]
523534
#[inline]
524535
unsafe fn backward_unchecked(start: char, count: usize) -> char {
525536
let start = start as u32;

0 commit comments

Comments
 (0)