Skip to main content

AsVirtPtr

Trait AsVirtPtr 

Source
pub trait AsVirtPtr {
    // Required method
    exec fn as_virt_ptr(&self) -> VirtPtr;
}
Expand description

Extension trait for byte slices that produces a VirtPtr covering the slice’s bytes. Mirrors the role of [<[u8]>::as_ptr] but in our verified pointer model.

Required Methods§

Source

exec fn as_virt_ptr(&self) -> VirtPtr

Implementations on Foreign Types§

Source§

impl AsVirtPtr for [u8]

Source§

exec fn as_virt_ptr(&self) -> r : VirtPtr

ensures
r.inv(),
r.range@.start == r.vaddr,
r.range@.end - r.range@.start == self.len(),

Implementors§