File tree Expand file tree Collapse file tree 1 file changed +3
-0
lines changed Expand file tree Collapse file tree 1 file changed +3
-0
lines changed Original file line number Diff line number Diff line change @@ -453,6 +453,7 @@ impl AsciiChar {
453453 /// or returns `None` if it's too large.
454454 #[ unstable( feature = "ascii_char" , issue = "110998" ) ]
455455 #[ inline]
456+ #[ ensures( |result| ( b <= 127 ) == ( result. is_some( ) && result. unwrap( ) as u8 == b) ) ]
456457 pub const fn from_u8 ( b : u8 ) -> Option < Self > {
457458 if b <= 127 {
458459 // SAFETY: Just checked that `b` is in-range
@@ -470,6 +471,8 @@ impl AsciiChar {
470471 /// `b` must be in `0..=127`, or else this is UB.
471472 #[ unstable( feature = "ascii_char" , issue = "110998" ) ]
472473 #[ inline]
474+ #[ requires( b <= 127 ) ]
475+ #[ ensures( |result| * result as u8 == b) ]
473476 pub const unsafe fn from_u8_unchecked ( b : u8 ) -> Self {
474477 // SAFETY: Our safety precondition is that `b` is in-range.
475478 unsafe { transmute ( b) }
You can’t perform that action at this time.
0 commit comments