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 11typedef seL4_Uint32 seL4_Word; 12typedef seL4_Word seL4_NodeId; 13typedef seL4_Word seL4_PAddr; 14typedef seL4_Word seL4_Domain; 15 16typedef seL4_Word seL4_CPtr; 17 18/* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */ 19typedef struct seL4_UserContext_ { 20 /* frameRegisters */ 21 seL4_Word eip, esp, eflags, eax, ebx, ecx, edx, esi, edi, ebp; 22 /* gpRegisters */ 23 seL4_Word fs_base, gs_base; 24} seL4_UserContext; 25 26