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