1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #pragma once
8 
9 #include <sel4/config.h>
10 
11 /* Set ENABLE_SMP_SUPPORT for kernel source files */
12 #ifdef CONFIG_ENABLE_SMP_SUPPORT
13 #define ENABLE_SMP_SUPPORT
14 #endif
15 
16 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
17 #ifdef CONFIG_ARM_PA_SIZE_BITS_40
18 #define AARCH64_VSPACE_S2_START_L1
19 #endif
20 #endif
21