aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/frame.sats
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/memory/frame.sats')
-rw-r--r--kernel/memory/frame.sats8
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats
index d965567..0de5056 100644
--- a/kernel/memory/frame.sats
+++ b/kernel/memory/frame.sats
@@ -17,7 +17,9 @@ typedef frame_allocator_t = @{
vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l)
-fn containing_address {l : addr} (address : ptr l) : frame_t
-fn allocate_frame {l : agz}{k : agz} (pf : !frame_allocator_t @ l >> frame_allocator_t @ l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : frame_t
+abst@ype frame_allocator = frame_allocator_t
+
+fn containing_address {l : addr} (address : ptr l) :<> frame_t
+fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) :<!ref,!wrt> frame_t
fn deallocate_frame (p : !allocptr) : void
-fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : allocptr
+fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void