From 7fce269442cb37810a14d088ea4a61d040ec3066 Mon Sep 17 00:00:00 2001 From: Xander Date: Sun, 20 Aug 2023 14:15:29 +0200 Subject: Rewrite table --- kernel/memory/paging/entry.sats | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'kernel/memory/paging/entry.sats') 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) : 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 -- cgit v1.2.3