1 /*
2  * Copyright 2014, General Dynamics C4 Systems
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #include <config.h>
8 #include <mode/model/statedata.h>
9 
10 /* Current active page directory. This is really just a shadow of CR3 */
11 UP_STATE_DEFINE(paddr_t, ia32KSCurrentPD VISIBLE);
12 
13 /* The privileged kernel mapping PD & PT */
14 pde_t ia32KSGlobalPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits));
15 pte_t ia32KSGlobalPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits));
16 
17 #ifdef CONFIG_KERNEL_LOG_BUFFER
18 pte_t ia32KSGlobalLogPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits));
19 #endif /* CONFIG_KERNEL_LOG_BUFFER */
20