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 #define SEL4_MAPPING_LOOKUP_LEVEL 2
10 #define SEL4_MAPPING_LOOKUP_NO_PT 21
11 #define SEL4_MAPPING_LOOKUP_NO_PD 30
12 #define SEL4_MAPPING_LOOKUP_NO_PUD 39
13 
seL4_MappingFailedLookupLevel(void)14 LIBSEL4_INLINE_FUNC seL4_Word seL4_MappingFailedLookupLevel(void)
15 {
16     return seL4_GetMR(SEL4_MAPPING_LOOKUP_LEVEL);
17 }
18