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