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 */
11UP_STATE_DEFINE(paddr_t, ia32KSCurrentPD VISIBLE);
12
13/* The privileged kernel mapping PD & PT */
14pde_t ia32KSGlobalPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits));
15pte_t ia32KSGlobalPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits));
16
17#ifdef CONFIG_KERNEL_LOG_BUFFER
18pte_t ia32KSGlobalLogPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits));
19#endif /* CONFIG_KERNEL_LOG_BUFFER */
20