Skip to main content

vm_space_reader_embedded

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

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(),
res matches Some(o) ==> o.mem_view is None,
res is Some ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,

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

Exec ensures reader_owner@.unwrap().mem_view is None (vm_space.rs:323).