diff options
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 |