diff options
| author | Xander <xander@biltopia.org> | 2023-07-27 00:46:53 +0200 |
|---|---|---|
| committer | Xander <xander@biltopia.org> | 2023-07-27 00:46:53 +0200 |
| commit | 54435375f29152ddbce1cd362a137280450eba94 (patch) | |
| tree | bed15b05a43d77d87977d35e337252577b46c92c /kernel/memory/frame.sats | |
| parent | 6cacc45cdf11ca0e605bb7c6356c569c8aed760b (diff) | |
| download | ats-os-54435375f29152ddbce1cd362a137280450eba94.tar.xz ats-os-54435375f29152ddbce1cd362a137280450eba94.zip | |
migrated frame_allocator to opt. side effects constrains not implemented yet
Diffstat (limited to 'kernel/memory/frame.sats')
| -rw-r--r-- | kernel/memory/frame.sats | 8 |
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 |