blob: 7320e3389ebb96441529e57487162b3f26319219 [file] [log] [blame]
/*
* Copyright 2017, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(DATA61_BSD)
*/
#include <sel4/sel4.h>
#include <stdio.h>
#include <stdlib.h>
#include <utils/util.h>
#include <sel4runtime.h>
seL4_BootInfo *platsupport_get_bootinfo(void)
{
/* bootinfo was set as an environment variable in _sel4_start */
seL4_BootInfo *bootinfo = sel4runtime_bootinfo();
if (!bootinfo) {
ZF_LOGE("Attempted %s in an environment without bootinfo.", __FUNCTION__);
return NULL;
}
/* Save the address of the IPC buffer for seL4_GetIPCBuffer on IA32. */
seL4_SetUserData((seL4_Word)bootinfo->ipcBuffer);
return bootinfo;
}
seL4_CPtr sel4ps_get_seL4_CapInitThreadTCB(void)
{
return seL4_CapInitThreadTCB;
}