hifitime 4.3.0

Ultra-precise date and time handling in Rust for scientific applications with leap second support
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

/*
* Hifitime
* Copyright (C) 2017-onward Christopher Rabotin <christopher.rabotin@gmail.com> et al. (cf. https://github.com/nyx-space/hifitime/graphs/contributors)
* This Source Code Form is subject to the terms of the Mozilla Public
* License, v. 2.0. If a copy of the MPL was not distributed with this
* file, You can obtain one at https://mozilla.org/MPL/2.0/.
*
* Documentation: https://nyxspace.com/
*/
use super::{
    format::Format,
    formatter::{Formatter, Item},
};
use crate::parser::Token;

#[cfg(kani)]
#[allow(non_snake_case)]
mod kani_harnesses {
    use super::*;
    use crate::*;
    #[kani::proof]
    fn kani_harness_need_gregorian() {
        let callee: Format = kani::any();
        let _ = 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();
        let _ = 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();
        let _ = 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();
        let _ = 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();
        let _ = 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();
        let _ = 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();
        let _ = 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();
        let _ = Formatter::with_timezone(epoch, offset, format);
    }

    #[kani::proof]
    #[kani::stub_verified(epoch::Epoch::to_time_scale)]
    fn kani_harness_Formatter_to_time_scale() {
        let dur: Duration = kani::any();
        let time_scale: TimeScale = kani::any();
        let epoch = Epoch::from_duration(dur, time_scale);
        let format: Format = kani::any();
        let time_scale: TimeScale = kani::any();
        let _ = 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();
        let _ = callee.set_timezone(offset);
    }
}