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 <autoconf.h>
10 #include <sel4/simple_types.h>
11 
12 typedef seL4_CPtr seL4_X64_PML4;
13 
14 /* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */
15 
16 typedef struct seL4_UserContext_ {
17     seL4_Word rip, rsp, rflags, rax, rbx, rcx, rdx, rsi, rdi, rbp,
18               r8, r9, r10, r11, r12, r13, r14, r15;
19     seL4_Word fs_base, gs_base;
20 } seL4_UserContext;
21