diff options
| author | Xander <xander@biltopia.org> | 2023-08-20 14:15:29 +0200 |
|---|---|---|
| committer | Xander <xander@biltopia.org> | 2023-08-20 14:15:29 +0200 |
| commit | 7fce269442cb37810a14d088ea4a61d040ec3066 (patch) | |
| tree | 61d1d0ac12e6eee71c1338db0f17e70691f499ce /kernel/memory/paging/entry.sats | |
| parent | 5e0dafa7cfbb90c941fc771f0d157cf13dc1aa91 (diff) | |
| download | ats-os-7fce269442cb37810a14d088ea4a61d040ec3066.tar.xz ats-os-7fce269442cb37810a14d088ea4a61d040ec3066.zip | |
Rewrite table
Diffstat (limited to 'kernel/memory/paging/entry.sats')
| -rw-r--r-- | kernel/memory/paging/entry.sats | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats index 2d12dbf..17a9f72 100644 --- a/kernel/memory/paging/entry.sats +++ b/kernel/memory/paging/entry.sats @@ -1,16 +1,9 @@ staload "kernel/memory/frame.sats" staload "lib/SATS/valid.sats" -abstype vaddr_type(l:addr) = ptr(l) -typedef vaddr(l:addr) = vaddr_type(l) - abst@ype entry_type = uint64 typedef entry_t = entry_type -typedef page_t = @{ - num = size_t -} - datatype entry_flag = | PRESENT | WRITABLE @@ -24,9 +17,9 @@ datatype entry_flag = | NO_EXECUTE fn is_unused(entry_t) : bool -fn set_unused(&entry_t) : void +fn set_unused(&entry_t) :<!wrt> void -fn contains_flag(entry_t,entry_flag) : bool +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 |