verdict_parser/x509/
time.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6// In X.509:
7// Time ::= CHOICE {
8//     utcTime        UTCTime, // more common
9//     generalTime    GeneralizedTime
10// }
11asn1! {
12    choice Time {
13        UTCTime(ASN1(UTCTime)): ASN1<UTCTime>,
14        GeneralizedTime(ASN1(GeneralizedTime)): ASN1<GeneralizedTime>,
15    }
16}
17
18}
19
20#[cfg(test)]
21mod test {
22    use super::*;
23
24    verus! {
25        /// Check that all trait bounds and preconditions are satisfied
26        #[test]
27        fn is_combinator() {
28            let _ = Time.parse(&[]);
29        }
30    }
31
32    #[test]
33    fn sanity() {
34        assert!(Time
35            .parse(&[
36                0x17, 0x0D, 0x31, 0x36, 0x30, 0x32, 0x30, 0x34, 0x31, 0x32, 0x33, 0x32, 0x32, 0x33,
37                0x5A,
38            ])
39            .is_ok());
40    }
41}