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