diff options
| author | Xander <xander@biltopia.org> | 2023-08-20 22:57:07 +0200 |
|---|---|---|
| committer | Xander <xander@biltopia.org> | 2023-08-20 23:03:17 +0200 |
| commit | 70cca66089896730797a71ba545c7f4e87b12975 (patch) | |
| tree | 167a22d505b32bf80bd8b432833e12a74a98941b /kernel/memory/paging/entry.sats | |
| parent | 7fce269442cb37810a14d088ea4a61d040ec3066 (diff) | |
| download | ats-os-70cca66089896730797a71ba545c7f4e87b12975.tar.xz ats-os-70cca66089896730797a71ba545c7f4e87b12975.zip | |
Diffstat (limited to 'kernel/memory/paging/entry.sats')
| -rw-r--r-- | kernel/memory/paging/entry.sats | 4 |
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 |