Function generalized_timevalue 

pub exec fn generalized_timevalue<'a>(bytes: &'a [u8]) -> res : Option<GeneralizedTime<'a>>

requires

generalized_time_bytes_wf::<false>(bytes@),

ensures

res.deep_view() == generalized_time_value(bytes@),

Verified executable implementation of generalized_time_value. Decodes the byte sequence into a GeneralizedTime.