From 6a3380f6d1320d8ccb4e5d39b08602b787dc2d47 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 9 Sep 2024 10:54:08 -0400 Subject: [PATCH] ascii_char contracts --- library/core/src/ascii/ascii_char.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs index 98e985bdc90b7..29f4c041e166d 100644 --- a/library/core/src/ascii/ascii_char.rs +++ b/library/core/src/ascii/ascii_char.rs @@ -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 { if b <= 127 { // SAFETY: Just checked that `b` is in-range @@ -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) }