Skip to main content

axiom_vm_io_entry_new

ostd::specs::mm::embedding

Function axiom_vm_io_entry_new 

Source 
pub proof fn axiom_vm_io_entry_new<'a>(
    vm_space: Option<VmSpaceId>,
    kind: VmIoKind,
    vaddr: Vaddr,
    len: usize,
tracked     owner: VmIoOwner,
) -> tracked res : VmIoEntry
Expand description
ensures
res.vm_space == vm_space,
res.kind == kind,
res.vaddr == vaddr,
res.len == len,
res.owner == owner,

Tracked constructor for VmIoEntry.