Skip to content

Commit 889b8cd

Browse files
committed
Use autoharness for char::convert::from_u32_unchecked
1 parent 2fd26a6 commit 889b8cd

File tree

2 files changed

+1
-12
lines changed

2 files changed

+1
-12
lines changed

.github/workflows/kani.yml

+1
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ jobs:
8181
scripts/run-kani.sh --run autoharness --kani-args \
8282
--include-pattern alloc::layout::Layout::from_size_align \
8383
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \
84+
--include-pattern char::convert::from_u32_unchecked \
8485
--include-pattern ptr::align_offset::mod_inv \
8586
--include-pattern ptr::alignment::Alignment::as_nonzero \
8687
--include-pattern ptr::alignment::Alignment::as_usize \

library/core/src/char/convert.rs

-12
Original file line numberDiff line numberDiff line change
@@ -288,15 +288,3 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
288288
None
289289
}
290290
}
291-
292-
#[cfg(kani)]
293-
#[unstable(feature = "kani", issue = "none")]
294-
mod verify {
295-
use super::*;
296-
297-
#[kani::proof_for_contract(from_u32_unchecked)]
298-
fn check_from_u32_unchecked() {
299-
let i: u32 = kani::any();
300-
unsafe { from_u32_unchecked(i) };
301-
}
302-
}

0 commit comments

Comments
 (0)