Add safety post-condition to unicode functions

Author: celinval

library/core/src/unicode/mod.rs

@@ -41,11 +41,12 @@ mod verify {
 
     /// Wrapper functions used to verify auto-generated functions from this module.
     ///
-    /// The files in this module is auto-generated by a script, so they are harder to annotate.
-    /// Instead, for each function that we want to verify, we create a wrapper function and add
-    /// contracts for them instead.
+    /// The files in this module are auto-generated by a script, so they are harder to annotate.
+    /// Instead, for each function that we want to verify, we create a wrapper function with
+    /// contracts.
     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());
     }
 }