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#ifdef HAVE_AUTOCONF 10#include <autoconf.h> 11#endif /* HAVE_AUTOCONF */ 12 13typedef enum _mode_object { 14 seL4_X86_PDPTObject = seL4_NonArchObjectTypeCount, 15 seL4_X64_PML4Object, 16#ifdef CONFIG_HUGE_PAGE 17 seL4_X64_HugePageObject, 18#endif 19 seL4_ModeObjectTypeCount 20} seL4_seL4ArchObjectType; 21 22/* allow seL4_X86_PDPTObject and seL4_IA32_PDPTObject to be used interchangeable */ 23#define seL4_IA32_PDPTObject seL4_X86_PDPTObject 24 25#ifndef CONFIG_HUGE_PAGE 26#define seL4_X64_HugePageObject 0xfffffffe 27#endif 28 29