Struct GeneralizedTime 

pub struct GeneralizedTime<'a> {
    pub datetime: DateTime,
    pub precision: TimePrecision,
    pub fraction: &'a [u8],
    pub zone: TimeZone,
}

Fields

datetime: DateTime

precision: TimePrecision

fraction: &'a [u8]

zone: TimeZone

Implementations

impl<'a> GeneralizedTime<'a>

pub exec fn new( datetime: DateTime, precision: TimePrecision, fraction: &'a [u8], zone: TimeZone, ) -> value : Self

requires

(GeneralizedTimeSpec {
    datetime,
    precision,
    fraction: fraction@,
    zone,
})
    .wf(),

ensures

value.deep_view()
    == (GeneralizedTimeSpec {
        datetime,
        precision,
        fraction: fraction@,
        zone,
    }),

pub exec fn fraction(&self) -> fraction : &'a [u8]

ensures

fraction.deep_view() == self.deep_view().fraction,

Trait Implementations

impl<'i, const DER: bool> ByteLen<GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

exec fn length(&self, value: &GeneralizedTime<'i>) -> usize

fn exec_inv(&self) -> bool

impl<'a> Clone for GeneralizedTime<'a>

fn clone(&self) -> GeneralizedTime<'a>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'a> Debug for GeneralizedTime<'a>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'a> DeepView for GeneralizedTime<'a>

closed spec fn deep_view(&self) -> Self::V

type V = GeneralizedTimeSpec

impl<'a> DerOrd<GeneralizedTime<'a>> for GeneralizedTimeFmt<true>

proof fn lemma_der_serialize_len(&self, value: GeneralizedTimeSpec)

open spec fn der_remaining( &self, value: GeneralizedTimeSpec, state: GeneralizedTimeDerState, ) -> Seq<u8>

{ self.spec_serialize(value).skip(state.pos as int) }

open spec fn der_state_valid( &self, value: GeneralizedTimeSpec, state: GeneralizedTimeDerState, ) -> bool

{
    &&& state.pos <= self.spec_serialize(value).len()
    &&& state.prefix@ == crate::asn1::generalizedtime::generalized_time_prefix(value)

}

exec fn der_start(&self, t: &GeneralizedTime<'a>) -> state : GeneralizedTimeDerState

exec fn der_next( &self, t: &GeneralizedTime<'a>, state: &mut GeneralizedTimeDerState, ) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl<'a> PartialEq for GeneralizedTime<'a>

fn eq(&self, other: &GeneralizedTime<'a>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<'i, const DER: bool> Prepare<GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

exec fn prepare( &self, value: &GeneralizedTime<'i>, ) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<'i, Output: OutputBuf, const DER: bool> Serializer<Output, GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

exec fn serialize_into(&self, value: &GeneralizedTime<'i>, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<'a> Copy for GeneralizedTime<'a>

impl<'a> Eq for GeneralizedTime<'a>

impl<'a> StructuralPartialEq for GeneralizedTime<'a>