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