Skip to main content

vm_space_cursor_mut_embedded

ostd::specs::mm::vm_space_embedding

Function vm_space_cursor_mut_embedded 

Source 
pub proof fn vm_space_cursor_mut_embedded<'a, 'rcu>(tracked 
    vm_space: &VmSpaceOwner,
    va: Range<Vaddr>,
) -> tracked res : Option<CursorOwner<'rcu, UserPtConfig>>
Expand description
requires
vm_space.inv(),
ensures
res matches Some(c) ==> c.inv(),

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

Same shape as vm_space_cursor_embedded.