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 */
17seL4_BootInfo *bootinfo;
18
19/** Consider moving seL4_InitBootInfo into libsel4_startup */
20void seL4_InitBootInfo(seL4_BootInfo *bi)
21{
22    bootinfo = bi;
23}
24
25seL4_BootInfo *seL4_GetBootInfo()
26{
27    return bootinfo;
28}
29