Skip to content

Commit

Permalink
ascii_char contracts
Browse files Browse the repository at this point in the history
  • Loading branch information
carolynzech committed Sep 9, 2024
1 parent 024e4c2 commit 6a3380f
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions library/core/src/ascii/ascii_char.rs
Original file line number Diff line number Diff line change
Expand Up @@ -453,6 +453,7 @@ impl AsciiChar {
/// or returns `None` if it's too large.
#[unstable(feature = "ascii_char", issue = "110998")]
#[inline]
#[ensures(|result| (b <= 127) == (result.is_some() && result.unwrap() as u8 == b))]
pub const fn from_u8(b: u8) -> Option<Self> {
if b <= 127 {
// SAFETY: Just checked that `b` is in-range
Expand All @@ -470,6 +471,8 @@ impl AsciiChar {
/// `b` must be in `0..=127`, or else this is UB.
#[unstable(feature = "ascii_char", issue = "110998")]
#[inline]
#[requires(b <= 127)]
#[ensures(|result| *result as u8 == b)]
pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
// SAFETY: Our safety precondition is that `b` is in-range.
unsafe { transmute(b) }
Expand Down

0 comments on commit 6a3380f

Please sign in to comment.