1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#pragma once 8 9#include <stdint.h> 10#include <api/types.h> 11#include <object/structures.h> 12#include <arch/types.h> 13 14struct pde_range { 15 pde_t *base; 16 word_t length; 17}; 18typedef struct pde_range pde_range_t; 19 20struct pte_range { 21 pte_t *base; 22 word_t length; 23}; 24typedef struct pte_range pte_range_t; 25 26typedef cte_t *cte_ptr_t; 27 28struct extra_caps { 29 cte_ptr_t excaprefs[seL4_MsgMaxExtraCaps]; 30}; 31typedef struct extra_caps extra_caps_t; 32 33