blob: 1de50c63d503101abc65c2e463214cc4345882d7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
staload FRAME = "kernel/memory/frame.sats"
staload "lib/SATS/valid.sats"
staload "./entry.sats"
typedef vaddr = Ptr0
typedef page_t = @{
num = size_t
}
fn translate(vaddr) : Valid $FRAME.paddr
fn containing_address(vaddr) : page_t
fn map_to{n:nat}(page_t,$FRAME.frame_t,&(@[entry_flag][n]),size : size_t n): void
fn map{n:nat}(page_t,&(@[entry_flag][n]),size : size_t n) : void
|
