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