blob: 17a9f723405473361b8d884f9aa7d3b5af66f494 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
staload "kernel/memory/frame.sats"
staload "lib/SATS/valid.sats"
abst@ype entry_type = uint64
typedef entry_t = entry_type
datatype entry_flag =
| PRESENT
| WRITABLE
| USER_ACCESSIBLE
| WRITE_THROUGH
| NO_CACHE
| ACCESSED
| DIRTY
| HUGE_PAGE
| GLOBAL
| NO_EXECUTE
fn is_unused(entry_t) : bool
fn set_unused(&entry_t) :<!wrt> void
fn contains_flag(entry_t,entry_flag):<> bool
fn pointed_frame(entry_t) : Valid frame_t
fn entry_set{n:nat}(&entry_t,frame_t,&(@[entry_flag][n]),size_t n) : void
|
