diff options
Diffstat (limited to 'kernel/bootinfo')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 4 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 5 |
2 files changed, 4 insertions, 5 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 4df903e..9eee595 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -45,7 +45,7 @@ end end -extern castfn ui2sz (n : uint) : [n : nat] size_t n +extern castfn ui2sz (n : uint) :<> [n : nat] size_t n //------------Memory------------------------ @@ -59,7 +59,7 @@ end // TODO: here use optional datatype (fix runtime alloc) implement get_memory_mapping(pf | p,n) = ( - assertloc(n < get_memory_mappings_n(pf | p)); + (* assertloc(n < get_memory_mappings_n(pf | p)); *) $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p->memory_map.entries,n)) ) 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 |