diff options
Diffstat (limited to 'kernel/bootinfo/multiboot.sats')
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index 1a2e6db..cab885a 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -45,24 +45,23 @@ typedef boot_info_t = @{ elf_tag = elf_tag_t } -vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | ptr l) - -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 print_memory_mappings (p : !bootptr) : void // Print all available memory area's - -fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n -fn get_elf_header (p : !bootptr, n : size_t) : elf64_shdr_t -fn print_elf_headers (p : !bootptr) : void - -fn get_kernel_ranges (p : !bootptr) : (Ptr,Ptr) // (kernel start, kernel end) -fn get_multiboot_ranges (p : !bootptr) : (Ptr0,Ptr0) // (bootinfo start, bootinfo end) - macdef invalid_area = @{ base_addr = the_null_ptr, length = i2sz(1), type = 0u, reserved = 0u } + +fun init(p : Ptr1) :void + +fn get_memory_mappings_n () : [n:nat] size_t n +fn get_memory_mapping (n : size_t) : memory_area_t +fn print_memory_mappings () : void // Print all available memory area's + +(* fn get_elf_headers_n () : [n:nat] size_t n *) +(* fn get_elf_header (n : size_t) : elf64_shdr_t *) +(* fn print_elf_headers () : void *) +(**) +(* fn get_kernel_ranges () : (Ptr,Ptr) // (kernel start, kernel end) *) +(* fn get_multiboot_ranges () : (Ptr0,Ptr0) // (bootinfo start, bootinfo end) *) + |