aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging.sats
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/memory/paging.sats')
-rw-r--r--kernel/memory/paging.sats2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/memory/paging.sats b/kernel/memory/paging.sats
index 784f567..477e942 100644
--- a/kernel/memory/paging.sats
+++ b/kernel/memory/paging.sats
@@ -1,6 +1,7 @@
#define ENTRY_COUNT 512
staload "./frame.sats"
+staload "lib/SATS/valid.sats"
abstype paddr_type(l:addr) = ptr(l)
typedef paddr(l:addr) = paddr_type(l)
@@ -31,3 +32,4 @@ fn is_unused(entry_t) : bool
fn set_unused(&entry_t) : void
fn flag_contains(entry_t,entry_flag) : bool
+fn test() : [b : bool] valid(int,b)