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
12typedef seL4_Uint64 seL4_Word;
13typedef seL4_Word seL4_NodeId;
14typedef seL4_Word seL4_PAddr;
15typedef seL4_Word seL4_Domain;
16
17typedef seL4_Word seL4_CPtr;
18
19typedef seL4_CPtr seL4_X64_PML4;
20
21/* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */
22
23typedef struct seL4_UserContext_ {
24    seL4_Word rip, rsp, rflags, rax, rbx, rcx, rdx, rsi, rdi, rbp,
25              r8, r9, r10, r11, r12, r13, r14, r15;
26    seL4_Word fs_base, gs_base;
27} seL4_UserContext;
28
29