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@[i..j],

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@[0..n],

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@[n..],

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".

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