aboutsummaryrefslogtreecommitdiff
path: root/kernel/bootinfo
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/bootinfo')
-rw-r--r--kernel/bootinfo/multiboot.dats4
-rw-r--r--kernel/bootinfo/multiboot.sats10
2 files changed, 7 insertions, 7 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index 742c7ed..6ea7b00 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -23,7 +23,7 @@ implement boot_info_init (p : Ptr1) = let
in
case+ type of
| 6u => (
- boot_p->memory_map := $UN.ptr0_get<memory_map_t>(p);
+ boot_p->memory_map := $UN.ptr0_get<memory_areas_t>(p);
boot_p->memory_map.entries := ptr_add<uint32>(p,4)
)
| 9u => (
@@ -60,7 +60,7 @@ end
implement get_memory_mapping(p,n) = (
assertloc(n < get_memory_mappings_n(p));
- $UN.ptr0_get<memory_entry_t>(ptr_add<memory_entry_t>(p.2->memory_map.entries,n))
+ $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p.2->memory_map.entries,n))
)
implement print_memory_mappings(p) = let
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 0d89040..3909fdd 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -4,15 +4,15 @@ typedef tag_t = @{
size = [n : nat | n >= 8] uint n // Size of tag (not including padding)
}
-typedef memory_entry_t = @{
+typedef memory_area_t = @{
base_addr = Ptr1, // Start of physical address
- length = uint64, // Size of memory region in bytes
+ length = [n : nat | n > 0 ] size_t n , // Size of memory region in bytes (64 bits)
type = uint, // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information,
// 4: reserved memory (preserved on hibernation), Other: reserved area
reserved = uint 0
}
-typedef memory_map_t = @{
+typedef memory_areas_t = @{
tag = tag_t,
entry_size = [n : nat | n > 0 && n % 8 == 0] uint n,
entry_version = uint,
@@ -42,7 +42,7 @@ typedef elf64_shdr_t = @{
typedef boot_info_t = @{
total_size = uint, // total size of boot information
- memory_map = memory_map_t,
+ memory_map = memory_areas_t,
elf_tag = elf_tag_t
}
@@ -51,7 +51,7 @@ 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 (p : !bootptr) : [n:nat] size_t n
-fn get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t
+fn get_memory_mapping (p : !bootptr, n : size_t) : memory_area_t
fn print_memory_mappings (p : !bootptr) : void
fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n