1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: BSD-2-Clause
5  */
6 
7 #pragma once
8 
9 #include <sel4/simple_types.h>
10 
11 typedef seL4_CPtr seL4_ARM_PageUpperDirectory;
12 typedef seL4_CPtr seL4_ARM_PageGlobalDirectory;
13 /* whether the VSpace refers to a PageUpperDirectory or PageGlobalDirectory directly
14  * depends on the physical address size */
15 typedef seL4_CPtr seL4_ARM_VSpace;
16 
17 typedef struct seL4_UserContext_ {
18     /* frame registers */
19     seL4_Word pc, sp, spsr, x0, x1, x2, x3, x4, x5, x6, x7, x8, x16, x17, x18, x29, x30;
20     /* other integer registers */
21     seL4_Word x9, x10, x11, x12, x13, x14, x15, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28;
22     /* Thread ID registers */
23     seL4_Word tpidr_el0, tpidrro_el0;
24 } seL4_UserContext;
25