diff options
Diffstat (limited to 'kernel/bootinfo')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 8 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index ff10c40..518962d 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -9,7 +9,7 @@ staload UN = "prelude/SATS/unsafe.sats" local - // Private function + // Private functions extern castfn ui2sz (n : uint) :<> [n : nat] size_t n extern fn _get_memory_mappings_n(boot_info: !boot_info_t):<> [n:nat] size_t n extern fn _get_memory_mapping(boot_info: !boot_info_t,n : size_t):<> memory_area_t @@ -54,7 +54,7 @@ in if (type != 0u) then loop(boot_info,ptr_add<uint8>(p, next)) else - unsafe_init(boot_info) + unsafe_init(boot_info) //UNSAFE: end implement initialize$fwork<boot_info_t>(v) = ( @@ -73,13 +73,13 @@ in implement get_memory_mappings_n() = let implement exec$fwork<boot_info_t><size_t>(v) = _get_memory_mappings_n(v) in - exec<boot_info_t><size_t>(bootinfo_ref) + $effmask_wrt(exec<boot_info_t><size_t>(bootinfo_ref)) end implement get_memory_mapping(n) = let implement exec$fwork<boot_info_t><memory_area_t>(v) = _get_memory_mapping(v,n) in - exec<boot_info_t><memory_area_t>(bootinfo_ref) + $effmask_wrt(exec<boot_info_t><memory_area_t>(bootinfo_ref)) end implement print_memory_mappings() = let diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index 16be379..2dfa205 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -55,9 +55,9 @@ macdef invalid_area = @{ fun init(p : Ptr1) :void -fn get_memory_mappings_n () : size_t -fn get_memory_mapping (n : size_t) : memory_area_t -fn print_memory_mappings () : void // Print all available memory area's +fn get_memory_mappings_n () :<!ref> size_t +fn get_memory_mapping (n : size_t) :<!ref> memory_area_t +fn print_memory_mappings () :<!ref,!wrt> void // Print all available memory area's fn get_elf_headers_n () : size_t fn get_elf_header (n : size_t) : elf64_shdr_t |