Skip to main content

axiom_segment_entry_new

ostd::specs::mm::embedding

Function axiom_segment_entry_new 

Source 
pub proof fn axiom_segment_entry_new(range: Range<Paddr>) -> tracked res : SegmentEntry
Expand description
ensures
res.range == range,

Tracked constructor for SegmentEntry.