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 
9 #include <autoconf.h>
10 
11 #define SEL4_MAPPING_LOOKUP_LEVEL 2
12 
13 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
14 #define SEL4_MAPPING_LOOKUP_NO_PT 21
15 #else
16 #define SEL4_MAPPING_LOOKUP_NO_PT 20
17 #endif
18 
seL4_MappingFailedLookupLevel(void)19 LIBSEL4_INLINE_FUNC seL4_Word seL4_MappingFailedLookupLevel(void)
20 {
21     return seL4_GetMR(SEL4_MAPPING_LOOKUP_LEVEL);
22 }
23