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§
Sourceexec fn as_virt_ptr(&self) -> VirtPtr
exec fn as_virt_ptr(&self) -> VirtPtr
Implementations on Foreign Types§
Source§impl AsVirtPtr for [u8]
impl AsVirtPtr for [u8]
Source§exec fn as_virt_ptr(&self) -> r : VirtPtr
exec fn as_virt_ptr(&self) -> r : VirtPtr
ensures
r.inv(),r.range@.start == r.vaddr,r.range@.end - r.range@.start == self.len(),