Struct PrintableStringOwned 

pub struct PrintableStringOwned { /* private fields */ }

Owned PrintableString value used when the wire representation is assembled from multiple BER segments.

Implementations

impl PrintableStringOwned

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

requires

is_valid_printable_string_spec(vstd::utf8::encode_utf8(inner.deep_view())),

ensures

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

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

ensures

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

Trait Implementations

impl ByteLen<PrintableStringOwned> for PrintableStringFmt

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl DeepView for PrintableStringOwned

Available on crate feature alloc only.

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

type V = PrintableStringSpec

impl Pred<PrintableStringOwned> for NumericStringChars

Available on crate feature alloc only.

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

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

Available on crate feature alloc only.

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

impl Prepare<PrintableStringOwned> for PrintableStringFmt

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, PrintableStringOwned> for PrintableStringFmt

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool