Skip to main content

axiom_frame_entry_new

ostd::specs::mm::embedding

Function axiom_frame_entry_new 

Source 
pub proof fn axiom_frame_entry_new(paddr: Paddr) -> tracked res : FrameEntry
Expand description
ensures
res.paddr == paddr,

Tracked constructor for FrameEntry.