ostd/specs/mm/
cpu.rs

1use vstd::prelude::*;
2
3verus! {
4
5pub struct CpuId(u32);
6
7pub struct AtomicCpuSet;
8
9impl AtomicCpuSet {
10    #[verifier::external_body]
11    pub fn new(_initial: CpuSet) -> Self {
12        unimplemented!()
13    }
14}
15
16pub struct CpuSet {
17    pub cpus: Set<CpuId>,
18}
19
20impl CpuSet {
21    pub open spec fn new_empty_spec() -> Self {
22        Self { cpus: Set::empty() }
23    }
24
25    #[verifier::external_body]
26    #[verifier::when_used_as_spec(new_empty_spec)]
27    pub fn new_empty() -> Self
28        returns
29            Self::new_empty_spec(),
30    {
31        unimplemented!()
32    }
33}
34
35pub trait PinCurrentCpu {
36
37}
38
39} // verus!
ostd/specs/mm/cpu.rs

ostd/specs/mm/
cpu.rs
