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 
14 struct pde_range {
15     pde_t *base;
16     word_t length;
17 };
18 typedef struct pde_range pde_range_t;
19 
20 struct pte_range {
21     pte_t *base;
22     word_t length;
23 };
24 typedef struct pte_range pte_range_t;
25 
26 typedef cte_t *cte_ptr_t;
27 
28 struct extra_caps {
29     cte_ptr_t excaprefs[seL4_MsgMaxExtraCaps];
30 };
31 typedef struct extra_caps extra_caps_t;
32