1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#pragma once
14
15#include <stdint.h>
16#include <sel4/types.h>
17#include <sel4/sel4.h>
18
19typedef struct frame_type {
20    seL4_Word type;
21    seL4_Word vaddr_offset;
22    seL4_Word size_bits;
23} frame_type_t;
24
25#include <arch_frame_type.h>
26
27/* define a couple of constants to aid creating virtual reservations for
28 * mapping in all the frame types. This region needs to be big enough to
29 * hold one mapping of every frame (this can be simplified to being twice
30 * the size of the largest frame) and aligned to the largest frame size */
31#define VSPACE_RV_ALIGN_BITS (frame_types[0].size_bits)
32#define VSPACE_RV_SIZE (2 * BIT(VSPACE_RV_ALIGN_BITS))
33
34