Skip to main content

vm_writer_from_kernel_space_embedded

ostd::specs::mm::embedding::io

Function vm_writer_from_kernel_space_embedded 

Source 
pub proof fn vm_writer_from_kernel_space_embedded(
    vaddr: Vaddr,
    len: usize,
) -> tracked res : VmIoOwner
Expand description
ensures
res.inv(),
res.has_write_view(),

Mirror of crate::mm::io::VmWriter<Infallible>::from_kernel_space.

Exec ensures (line 787-795) that with fallible = false and under the kernel-VA range guard, the produced owner satisfies has_write_view(). Pre-activated as a Writer.