Skip to main content

seg_nframes

ostd::specs::mm::frame::segment

Function seg_nframes 

Source 
pub open spec fn seg_nframes(range: Range<Paddr>) -> int
Expand description
{ (range.end - range.start) / PAGE_SIZE as int }

A SegmentOwner<M> holds the permission tokens for all frames in the Segment<M> for verification purposes.

The range field tracks which physical-address range this owner corresponds to. It is a ghost-only field used by [Self::inv] to express the structural connection between perms and the segment’s frames. Number of frames in a page-aligned physical range.