Add safety post-condition to unicode functions

celinval · Oct 16, 2024 · 6ca2f3c · 6ca2f3c
1 parent d2e13b1
commit 6ca2f3c
Showing 1 changed file with 6 additions and 9 deletions.
diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs
@@ -46,6 +46,7 @@ mod verify {
     /// contracts for them instead.
     mod wrappers {
         use super::*;
+        use crate::ub_checks;
 
         /// Wraps `conversions::to_upper` function.
         ///
@@ -54,9 +55,7 @@ mod verify {
         /// # todo!()
         /// }
         /// ```
-        #[ensures(|res| c.is_ascii() == res[0].is_ascii())]
-        #[ensures(|res| if c.is_ascii() { &res[1..2] == &['\0', '\0'] } else { true })]
-        #[ensures(|res| if ('a'..'z').contains(&c) { ('A'..'Z').contains(&res[0]) } else { c == res[0] })]
+        #[ensures(|res| ub_checks::can_dereference(res))]
         pub fn to_upper_wrapper(c: char) -> [char; 3] {
             to_upper(c)
         }
@@ -68,21 +67,19 @@ mod verify {
         /// # todo!()
         /// }
         /// ```
-        #[ensures(|res| c.is_ascii() == res[0].is_ascii())]
-        #[ensures(|res| if c.is_ascii() { &res[1..2] == &['\0', '\0'] } else { true })]
-        #[ensures(|res| if ('A'..'Z').contains(&c) { ('a'..'z').contains(&res[0]) } else { c == res[0] })]
+        #[ensures(|res| ub_checks::can_dereference(res))]
         pub fn to_lower_wrapper(c: char) -> [char; 3] {
             to_lower(c)
         }
     }
 
     #[kani::proof_for_contract(to_upper_wrapper)]
-    fn check_to_upper() {
+    fn check_to_upper_safety() {
         let _ = to_upper_wrapper(kani::any());
     }
 
     #[kani::proof_for_contract(to_lower_wrapper)]
-    fn check_to_lower() {
-        let _ = to_upper_wrapper(kani::any());
+    fn check_to_lower_safety() {
+        let _ = to_lower_wrapper(kani::any());
     }
 }