1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: BSD-2-Clause
5  */
6 
7 #include <sel4/sel4.h>
8 
9 #ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
10 __thread char __sel4_print_error = CONFIG_LIB_SEL4_PRINT_INVOCATION_ERRORS;
11 #endif
12 
13 /** Userland per-thread IPC buffer address **/
14 __thread seL4_IPCBuffer *__sel4_ipc_buffer;
15 
16 /** Consider moving bootinfo into libsel4_startup */
17 seL4_BootInfo *bootinfo;
18 
19 /** Consider moving seL4_InitBootInfo into libsel4_startup */
seL4_InitBootInfo(seL4_BootInfo * bi)20 void seL4_InitBootInfo(seL4_BootInfo *bi)
21 {
22     bootinfo = bi;
23 }
24 
seL4_GetBootInfo()25 seL4_BootInfo *seL4_GetBootInfo()
26 {
27     return bootinfo;
28 }
29