Struct BitStringOwned 

pub struct BitStringOwned { /* private fields */ }

Owned BIT STRING value used when BER segments must be flattened.

Implementations

impl BitStringOwned

pub exec fn new(unused: u8, bits: Vec<u8>) -> value : Self

requires

unused <= 7,

bits.len() == 0 ==> unused == 0,

ensures

value.deep_view()
    == (BitStringSpec {
        unused,
        bits: bits.deep_view(),
    }),

pub exec fn unused(&self) -> unused : u8

ensures

unused == self.deep_view().unused,

self.deep_view().wf::<false>(),

pub exec fn bits(&self) -> bits : &[u8]

ensures

bits.deep_view() == self.deep_view().bits,

Trait Implementations

impl ByteLen<BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl DeepView for BitStringOwned

Available on crate feature alloc only.

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

type V = BitStringSpec

impl Prepare<BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool