Skip to main content

count_present_upto

ostd::specs::mm::page_table::node::owners

Function count_present_upto 

Source 
pub open spec fn count_present_upto<E: PageTableEntryTrait>(s: Seq<E>, n: int) -> int
Expand description
{
    if n <= 0 {
        0
    } else {
        count_present_upto(s, n - 1) + if s[n - 1].is_present() { 1int } else { 0int }
    }
}

Number of present PTEs among the first n entries of s.