aboutsummaryrefslogtreecommitdiff
path: root/kernel/bootinfo/multiboot.sats
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-07-27 00:46:53 +0200
committerXander <xander@biltopia.org>2023-07-27 00:46:53 +0200
commit54435375f29152ddbce1cd362a137280450eba94 (patch)
treebed15b05a43d77d87977d35e337252577b46c92c /kernel/bootinfo/multiboot.sats
parent6cacc45cdf11ca0e605bb7c6356c569c8aed760b (diff)
downloadats-os-54435375f29152ddbce1cd362a137280450eba94.tar.xz
ats-os-54435375f29152ddbce1cd362a137280450eba94.zip
migrated frame_allocator to opt. side effects constrains not implemented yet
Diffstat (limited to 'kernel/bootinfo/multiboot.sats')
-rw-r--r--kernel/bootinfo/multiboot.sats5
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 684286b..1a2e6db 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -1,4 +1,3 @@
-
typedef tag_t = @{
type = uint32, // Identifier of tag
size = [n : nat | n >= 8] uint n // Size of tag (not including padding)
@@ -50,8 +49,8 @@ vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | p
fun boot_info_init(p : Ptr1) : bootptr
-fn get_memory_mappings_n {l : agz} (pf : !boot_info_t@l | p : ptr l) : [n:nat] size_t n
-fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) : memory_area_t
+fn get_memory_mappings_n {l : agz} (pf : !boot_info_t@l | p : ptr l) :<> [n:nat] size_t n
+fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) :<> memory_area_t
fn print_memory_mappings (p : !bootptr) : void // Print all available memory area's
fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n