Skip to main content

vm_space_writer_embedded

ostd::specs::mm::vm_space_embedding

Function vm_space_writer_embedded 

Source 
pub proof fn vm_space_writer_embedded<'a>(tracked 
    vm_space: &VmSpaceOwner,
    vaddr: Vaddr,
    len: usize,
) -> tracked res : Option<VmIoOwner>
Expand description
requires
vm_space.inv(),
ensures
res matches Some(o) ==> o.inv(),

Mirror of crate::mm::vm_space::VmSpace::writer.