typedef tag_t = @{ type = uint32, // Identifier of tag size = [n : nat | n >= 8] uint n // Size of tag (not including padding) } typedef memory_area_t = @{ base_addr = Ptr, // Start of physical address 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_areas_t = @{ tag = tag_t, entry_size = [n : nat | n > 0 && n % 8 == 0] uint n, entry_version = uint, entries = ptr // Pointer to entries } typedef elf_tag_t = @{ tag = tag_t, num = uint, // Number of elf entries entsize = uint 64, // Size of entry shndx = uint, // Index of the section containing the string table headers = ptr // Pointer to entries } typedef elf64_shdr_t = @{ name = uint, // Index into seaction header string table type = uint, // Type of section (code,data,symbol,...) flags = uint64, // Attributes and flags of section addr = Ptr1, // (virtual) address of section in memory offset = Ptr1, // Offset of seaction in ELF executable file size = size_t, // Size of section in bytes link = uint, // Extra informaion info = uint, // Additional information addralign = uint64, // Alignment requirements of section's address entsize = size_t 64 // Size of each entry in section } typedef boot_info_t = @{ total_size = uint, // total size of boot information memory_map = memory_areas_t, elf_tag = elf_tag_t } 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) *)