1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: BSD-2-Clause
5  */
6 
7 #pragma once
8 #include <sel4/types.h>
9 #include <sel4/macros.h>
10 
11 #include <sel4/syscalls.h>
12 #include <sel4/arch/syscalls.h>
13 #include <sel4/sel4_arch/syscalls.h>
14 
15 #include <sel4/invocation.h>
16 #include <interfaces/sel4_client.h>
17 #include <sel4/virtual_client.h>
18 
19 #include <sel4/bootinfo.h>
20 #include <sel4/faults.h>
21 #include <sel4/deprecated.h>
22 #include <sel4/constants.h>
23 #include <sel4/sel4_arch/constants.h>
24 #include <sel4/arch/constants.h>
25 #include <sel4/plat/api/constants.h>
26 
27 
28