aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging.dats
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/memory/paging.dats')
-rw-r--r--kernel/memory/paging.dats6
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/memory/paging.dats b/kernel/memory/paging.dats
index 9b55624..84a8bf4 100644
--- a/kernel/memory/paging.dats
+++ b/kernel/memory/paging.dats
@@ -6,6 +6,7 @@ staload UN = "prelude/SATS/unsafe.sats"
staload "./paging.sats"
staload "./frame.sats"
+staload "lib/SATS/valid.sats"
assume entry_type = uint64
@@ -28,3 +29,8 @@ implement flag_contains(entry,flag) =
| NO_EXECUTE() => 63
))) != zero
+(* implement test() = let *)
+(* in *)
+(* (5,true) *)
+(* end *)
+