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 11typedef seL4_Uint32 seL4_Word; 12typedef seL4_Word seL4_CPtr; 13typedef seL4_Word seL4_NodeId; 14typedef seL4_Word seL4_PAddr; 15typedef seL4_Word seL4_Domain; 16 17typedef struct seL4_UserContext_ { 18 /* frame registers */ 19 seL4_Word pc, sp, cpsr, r0, r1, r8, r9, r10, r11, r12; 20 /* other integer registers */ 21 seL4_Word r2, r3, r4, r5, r6, r7, r14; 22 /* Thread ID registers */ 23 seL4_Word tpidrurw, tpidruro; 24} seL4_UserContext; 25 26