diff options
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 |