Skip to main content

vm_space_reader_embedded

ostd::specs::mm::vm_space_embedding

Function vm_space_reader_embedded 

Source 
pub proof fn vm_space_reader_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::reader.

On success returns Some with a VmIoOwner whose inv() holds. The real exec function may fail when vaddr+len exceeds the user-space range or the active page table doesn’t match this VmSpace; that failure is modeled by returning None.