Adrian Danis | 3ccebef | 2017-02-15 12:27:03 +1100 | [diff] [blame] | 1 | /* |
Gerwin Klein | 600fe15 | 2021-02-10 19:19:17 +1100 | [diff] [blame] | 2 | * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) |
Adrian Danis | 3ccebef | 2017-02-15 12:27:03 +1100 | [diff] [blame] | 3 | * |
Gerwin Klein | 600fe15 | 2021-02-10 19:19:17 +1100 | [diff] [blame] | 4 | * SPDX-License-Identifier: BSD-2-Clause |
Adrian Danis | 3ccebef | 2017-02-15 12:27:03 +1100 | [diff] [blame] | 5 | */ |
| 6 | |
| 7 | #pragma once |
| 8 | |
| 9 | #include <sel4/sel4.h> |
| 10 | #include <sel4/macros.h> |
| 11 | |
| 12 | /* Helper function for pulling the bootinfo pointer out of the environment. */ |
| 13 | seL4_BootInfo *platsupport_get_bootinfo(void); |
Adrian Danis | bd8018b | 2017-08-08 03:56:54 +1000 | [diff] [blame] | 14 | |
| 15 | /* Helper function for getting the value of seL4_CapInitThreadTCB, which is an enum, |
| 16 | * into assembly */ |
| 17 | seL4_CPtr sel4ps_get_seL4_CapInitThreadTCB(void); |