Trait InputBuf 

pub trait InputBuf: InputSlice + Sized {
    // Required methods
    exec fn len(&self) -> len : usize;
    exec fn subrange(&self, i: usize, j: usize) -> sliced : Self;

    // Provided methods
    exec fn take(&self, n: usize) -> taken : Self { ... }
    fn skip(&self, n: usize) -> Self { ... }
}

Trait for types that can be used as input for Vest parsers, roughly corresponding to byte buffers.

Required Methods

exec fn len(&self) -> len : usize

ensures

len == self@.len(),

The length of the buffer.

exec fn subrange(&self, i: usize, j: usize) -> sliced : Self

requires

0 <= i as int <= j as int <= self@.len(),

ensures

sliced@ == self@.subrange(i as int, j as int),

sliced.deep_view() == sliced@,

A slice-like view of the range [i, j) of the buffer.

Provided Methods

exec fn take(&self, n: usize) -> taken : Self

requires

n as int <= self@.len(),

ensures

taken@ == self@.take(n as int),

taken.deep_view() == taken@,

A view of the first n bytes of the buffer.

exec fn skip(&self, n: usize) -> skipped : Self

requires

n as int <= self@.len(),

ensures

skipped@ == self@.skip(n as int),

skipped.deep_view() == skipped@,

A view of the buffer with the first n bytes skipped.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<'input> InputBuf for &'input [u8]

exec fn len(&self) -> len : usize

exec fn subrange(&self, i: usize, j: usize) -> &'input [u8]

Implementors