Add autogenerated Kani harnesses

src/duration/kani_verif.rs

@@ -122,3 +122,230 @@ mod tests {
     // repeat_test!(test_dur_f64_recip_5, [1e4, 1e5]);
     // repeat_test!(test_dur_f64_recip_6, [1e5, 1e6]);
 }
+
+#[cfg(kani)]
+mod kani_harnesses {
+    use crate::Unit;
+    use super::*;
+    #[kani::proof]
+    fn kani_harness_Duration_from_parts() {
+        let centuries: i16 = kani::any();
+        let nanoseconds: u64 = kani::any();
+        Duration::from_parts(centuries, nanoseconds);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_total_nanoseconds() {
+        let nanos: i128 = kani::any();
+        Duration::from_total_nanoseconds(nanos);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_truncated_nanoseconds() {
+        let nanos: i64 = kani::any();
+        Duration::from_truncated_nanoseconds(nanos);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_days() {
+        let value: f64 = kani::any();
+        Duration::from_days(value);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_hours() {
+        let value: f64 = kani::any();
+        Duration::from_hours(value);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_seconds() {
+        let value: f64 = kani::any();
+        Duration::from_seconds(value);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_milliseconds() {
+        let value: f64 = kani::any();
+        Duration::from_milliseconds(value);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_microseconds() {
+        let value: f64 = kani::any();
+        Duration::from_microseconds(value);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_nanoseconds() {
+        let value: f64 = kani::any();
+        Duration::from_nanoseconds(value);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_compose() {
+        let sign: i8 = kani::any();
+        let days: u64 = kani::any();
+        let hours: u64 = kani::any();
+        let minutes: u64 = kani::any();
+        let seconds: u64 = kani::any();
+        let milliseconds: u64 = kani::any();
+        let microseconds: u64 = kani::any();
+        let nanoseconds: u64 = kani::any();
+        Duration::compose(
+            sign,
+            days,
+            hours,
+            minutes,
+            seconds,
+            milliseconds,
+            microseconds,
+            nanoseconds,
+        );
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_compose_f64() {
+        let sign: i8 = kani::any();
+        let days: f64 = kani::any();
+        let hours: f64 = kani::any();
+        let minutes: f64 = kani::any();
+        let seconds: f64 = kani::any();
+        let milliseconds: f64 = kani::any();
+        let microseconds: f64 = kani::any();
+        let nanoseconds: f64 = kani::any();
+        Duration::compose_f64(
+            sign,
+            days,
+            hours,
+            minutes,
+            seconds,
+            milliseconds,
+            microseconds,
+            nanoseconds,
+        );
+    }
+
+    #[kani::proof]
+    fn kani_harness_Duration_from_tz_offset() {
+        let sign: i8 = kani::any();
+        let hours: i64 = kani::any();
+        let minutes: i64 = kani::any();
+        Duration::from_tz_offset(sign, hours, minutes);
+    }
+
+    #[kani::proof]
+    fn kani_harness_normalize() {
+        let mut callee: Duration = kani::any();
+        callee.normalize();
+    }
+
+    #[kani::proof]
+    fn kani_harness_to_parts() {
+        let callee: Duration = kani::any();
+        callee.to_parts();
+    }
+
+    #[kani::proof]
+    fn kani_harness_total_nanoseconds() {
+        let callee: Duration = kani::any();
+        callee.total_nanoseconds();
+    }
+
+    #[kani::proof]
+    fn kani_harness_try_truncated_nanoseconds() {
+        let callee: Duration = kani::any();
+        callee.try_truncated_nanoseconds();
+    }
+
+    #[kani::proof]
+    fn kani_harness_truncated_nanoseconds() {
+        let callee: Duration = kani::any();
+        callee.truncated_nanoseconds();
+    }
+
+    #[kani::proof]
+    fn kani_harness_to_seconds() {
+        let callee: Duration = kani::any();
+        callee.to_seconds();
+    }
+
+    #[kani::proof]
+    fn kani_harness_to_unit() {
+        let unit: Unit = kani::any();
+        let callee: Duration = kani::any();
+        callee.to_unit(unit);
+    }
+
+    #[kani::proof]
+    fn kani_harness_abs() {
+        let callee: Duration = kani::any();
+        callee.abs();
+    }
+
+    #[kani::proof]
+    fn kani_harness_signum() {
+        let callee: Duration = kani::any();
+        callee.signum();
+    }
+
+    #[kani::proof]
+    fn kani_harness_decompose() {
+        let callee: Duration = kani::any();
+        callee.decompose();
+    }
+
+    #[kani::proof]
+    fn kani_harness_subdivision() {
+        let unit: Unit = kani::any();
+        let callee: Duration = kani::any();
+        callee.subdivision(unit);
+    }
+
+    #[kani::proof]
+    fn kani_harness_floor() {
+        let duration: Duration = kani::any();
+        let callee: Duration = kani::any();
+        callee.floor(duration);
+    }
+
+    #[kani::proof]
+    fn kani_harness_ceil() {
+        let duration: Duration = kani::any();
+        let callee: Duration = kani::any();
+        callee.ceil(duration);
+    }
+
+    #[kani::proof]
+    fn kani_harness_round() {
+        let duration: Duration = kani::any();
+        let callee: Duration = kani::any();
+        callee.round(duration);
+    }
+
+    #[kani::proof]
+    fn kani_harness_approx() {
+        let callee: Duration = kani::any();
+        callee.approx();
+    }
+
+    #[kani::proof]
+    fn kani_harness_min() {
+        let other: Duration = kani::any();
+        let callee: Duration = kani::any();
+        callee.min(other);
+    }
+
+    #[kani::proof]
+    fn kani_harness_max() {
+        let other: Duration = kani::any();
+        let callee: Duration = kani::any();
+        callee.max(other);
+    }
+
+    #[kani::proof]
+    fn kani_harness_is_negative() {
+        let callee: Duration = kani::any();
+        callee.is_negative();
+    }
+}

src/duration/mod.rs

@@ -827,4 +827,4 @@ mod ut_duration {
         assert_eq!(microseconds, 0);
         assert_eq!(nanoseconds, 0);
     }
-}
+}

src/efmt/format.rs

@@ -110,6 +110,7 @@ const MAX_TOKENS: usize = 16;
 /// let fmt = Formatter::new(bday, consts::RFC2822);
 /// assert_eq!(format!("{fmt}"), format!("Tue, 29 Feb 2000 14:57:29"));
 /// ```
+#[cfg_attr(kani, derive(kani::Arbitrary))]
 #[derive(Copy, Clone, Default, PartialEq)]
 pub struct Format {
     pub(crate) items: [Option<Item>; MAX_TOKENS],
@@ -599,4 +600,4 @@ fn gh_248_regression() {
     let e = Epoch::from_format_str("2023-117T12:55:26", "%Y-%jT%H:%M:%S").unwrap();
 
     assert_eq!(format!("{e}"), "2023-04-27T12:55:26 UTC");
-}
+}

src/efmt/formatter.rs

@@ -17,7 +17,7 @@ use super::format::Format;
 #[cfg(not(feature = "std"))]
 #[allow(unused_imports)] // Import is indeed used.
 use num_traits::Float;
-
+#[cfg_attr(kani, derive(kani::Arbitrary))]
 #[derive(Copy, Clone, Default, Debug, PartialEq)]
 pub(crate) struct Item {
     pub(crate) token: Token,
@@ -76,6 +76,7 @@ impl Item {
     }
 }
 
+#[cfg_attr(kani, derive(kani::Arbitrary))]
 #[derive(Copy, Clone, Debug, PartialEq)]
 pub struct Formatter {
     epoch: Epoch,
@@ -301,4 +302,4 @@ impl fmt::Display for Formatter {
         }
         Ok(())
     }
-}
+}

src/efmt/kani_verif.rs

@@ -0,0 +1,84 @@
+use super::{
+    format::Format,
+    formatter::{Item, Formatter},
+};
+use crate::{duration::Duration, TimeScale};
+use crate::Epoch;
+use crate::parser::Token;
+
+#[cfg(kani)]
+mod kani_harnesses {
+    use crate::*;
+    use super::*;
+    #[kani::proof]
+    fn kani_harness_need_gregorian() {
+        let callee: Format = kani::any();
+        callee.need_gregorian();
+    }
+
+    #[kani::proof]
+    fn kani_harness_Item_new() {
+        let token: Token = kani::any();
+        let sep_char: Option<char> = kani::any();
+        let second_sep_char: Option<char> = kani::any();
+        Item::new(token, sep_char, second_sep_char);
+    }
+
+    #[kani::proof]
+    fn kani_harness_sep_char_is() {
+        let c_in: char = kani::any();
+        let callee: Item = kani::any();
+        callee.sep_char_is(c_in);
+    }
+
+    #[kani::proof]
+    fn kani_harness_sep_char_is_not() {
+        let c_in: char = kani::any();
+        let callee: Item = kani::any();
+        callee.sep_char_is_not(c_in);
+    }
+
+    #[kani::proof]
+    fn kani_harness_second_sep_char_is() {
+        let c_in: char = kani::any();
+        let callee: Item = kani::any();
+        callee.second_sep_char_is(c_in);
+    }
+
+    #[kani::proof]
+    fn kani_harness_second_sep_char_is_not() {
+        let c_in: char = kani::any();
+        let callee: Item = kani::any();
+        callee.second_sep_char_is_not(c_in);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Formatter_new() {
+        let epoch: Epoch = kani::any();
+        let format: Format = kani::any();
+        Formatter::new(epoch, format);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Formatter_with_timezone() {
+        let epoch: Epoch = kani::any();
+        let offset: Duration = kani::any();
+        let format: Format = kani::any();
+        Formatter::with_timezone(epoch, offset, format);
+    }
+
+    #[kani::proof]
+    fn kani_harness_Formatter_to_time_scale() {
+        let epoch: Epoch = kani::any();
+        let format: Format = kani::any();
+        let time_scale: TimeScale = kani::any();
+        Formatter::to_time_scale(epoch, format, time_scale);
+    }
+
+    #[kani::proof]
+    fn kani_harness_set_timezone() {
+        let offset: Duration = kani::any();
+        let mut callee: Formatter = kani::any();
+        callee.set_timezone(offset);
+    }
+}

src/efmt/mod.rs

@@ -14,3 +14,6 @@ pub mod formatter;
 
 pub use format::Format;
 pub use formatter::Formatter;
+
+#[cfg(kani)]
+mod kani_verif;