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