aboutsummaryrefslogtreecommitdiff
path: root/kernel/multiboot.sats
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/multiboot.sats')
-rw-r--r--kernel/multiboot.sats34
1 files changed, 0 insertions, 34 deletions
diff --git a/kernel/multiboot.sats b/kernel/multiboot.sats
deleted file mode 100644
index 9cbc4b4..0000000
--- a/kernel/multiboot.sats
+++ /dev/null
@@ -1,34 +0,0 @@
-
-typedef tag_t = @{
- type = uint32, // Identifier of tag
- size = [n : nat | n >= 8] uint n // Size of tag (not including padding)
-}
-
-typedef memory_entry_t = @{
- base_addr = Ptr1, // Start of physical address
- length = uint64, // Size of memory region in bytes
- 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 = @{
- tag = tag_t,
- entry_size = [n : nat | n > 0 && n % 8 == 0] uint n,
- entry_version = uint,
- entries = ptr // Pointer to entries
-}
-
-
-typedef boot_info_t = @{
- total_size = uint, // total size of boot information
- memory_map = memory_map_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
-
-fun get_memory_mappings_n (p : !bootptr) : size_t
-
-fun get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t