blob: 0926e6c4564324c1fcaff6cfed4ed9d812e0b29f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
(* #define PAGE_SIZE 4096 *)
(**)
(* staload "kernel/bootinfo/multiboot.sats" *)
(**)
(* typedef frame_t = @{ *)
(* num = size_t *)
(* } *)
(**)
(* typedef frame_allocator_t = @{ *)
(* next_free_frame = frame_t, *)
(* current_area = memory_area_t, *)
(* kernel_start = frame_t, *)
(* kernel_end = frame_t, *)
(* multiboot_start = frame_t, *)
(* multiboot_end = frame_t *)
(* } *)
(**)
(* vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l) *)
(**)
(* abst@ype frame_allocator = frame_allocator_t *)
(**)
(* fn containing_address {l : addr} (address : ptr l) :<> frame_t *)
(* fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) :<!ref,!wrt> frame_t *)
(* fn deallocate_frame (p : !allocptr) : void *)
(* (* fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void *) *)
|
