aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging/entry.sats
blob: fc20a20f2b22b46d0cd39f4ce11e68c14d8e0346 (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
26
27
staload "kernel/memory/frame.sats"
staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"

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 add_flag(entry_t,entry_flag) : entry_t
fn create_entry{s:nat}(frame_t,&(@[entry_flag][s]),size_t s) : entry_t