Struct BmpString 

pub struct BmpString { /* private fields */ }

Semantic BMPString value. Parsing necessarily owns the result because BMPString wire octets are not UTF-8 and constructed BER values may span discontiguous input segments.

Implementations

impl BmpString

pub exec fn new(inner: String) -> res : Self

requires

is_valid_bmp_chars(inner.deep_view()),

ensures

res.deep_view()
    == (BmpStringSpec {
        inner: inner.deep_view(),
    }),

pub exec fn inner(&self) -> res : &str

ensures

res.deep_view() == self.deep_view().inner,

Trait Implementations

impl ByteLen<BmpString> for BmpStringFmt

Available on crate feature alloc only.

exec fn length(&self, v: &BmpString) -> usize

fn exec_inv(&self) -> bool

impl DeepView for BmpString

Available on crate feature alloc only.

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

type V = BmpStringSpec

impl DerOrd<BmpString> for BmpStringFmt

Available on crate feature alloc only.

proof fn lemma_der_serialize_len(&self, value: BmpStringSpec)

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

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

open spec fn der_state_valid( &self, value: BmpStringSpec, state: BmpStringDerState, ) -> bool

{
    &&& state.char_index <= value.inner.len()
    &&& state.char_index == value.inner.len() ==> !state.second_octet

}

exec fn der_start(&self, s: &BmpString) -> state : BmpStringDerState

exec fn der_next(&self, s: &BmpString, state: &mut BmpStringDerState) -> next : Option<u8>

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

impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<BmpString> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

Available on crate feature alloc only.

exec fn test(&self, value: &BmpString) -> ok : bool

impl Prepare<BmpString> for BmpStringFmt

Available on crate feature alloc only.

exec fn prepare(&self, v: &BmpString) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, BmpString> for BmpStringFmt

Available on crate feature alloc only.

exec fn serialize_into(&self, v: &BmpString, obuf: &mut Output)

fn exec_inv(&self) -> bool