aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging/entry.sats
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-08-20 22:57:07 +0200
committerXander <xander@biltopia.org>2023-08-20 23:03:17 +0200
commit70cca66089896730797a71ba545c7f4e87b12975 (patch)
tree167a22d505b32bf80bd8b432833e12a74a98941b /kernel/memory/paging/entry.sats
parent7fce269442cb37810a14d088ea4a61d040ec3066 (diff)
downloadats-os-master.tar.xz
ats-os-master.zip
implement pageHEADmaster
Diffstat (limited to 'kernel/memory/paging/entry.sats')
-rw-r--r--kernel/memory/paging/entry.sats4
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats
index 17a9f72..fc20a20 100644
--- a/kernel/memory/paging/entry.sats
+++ b/kernel/memory/paging/entry.sats
@@ -1,5 +1,6 @@
staload "kernel/memory/frame.sats"
staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
abst@ype entry_type = uint64
typedef entry_t = entry_type
@@ -22,4 +23,5 @@ fn set_unused(&entry_t) :<!wrt> void
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
+fn add_flag(entry_t,entry_flag) : entry_t
+fn create_entry{s:nat}(frame_t,&(@[entry_flag][s]),size_t s) : entry_t