ostd/specs/mm/
cpu.rs

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

ostd/specs/mm/cpu.rs

ostd/specs/mm/
cpu.rs