1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#ifndef __ARCH_OBJECTTYPE_H 14#define __ARCH_OBJECTTYPE_H 15 16#ifdef HAVE_AUTOCONF 17#include <autoconf.h> 18#endif /* HAVE_AUTOCONF */ 19 20typedef enum _object { 21 seL4_ARM_SmallPageObject = seL4_ModeObjectTypeCount, 22 seL4_ARM_LargePageObject, 23#ifdef CONFIG_ARCH_AARCH32 24 seL4_ARM_SectionObject, 25 seL4_ARM_SuperSectionObject, 26#endif 27 seL4_ARM_PageTableObject, 28 seL4_ARM_PageDirectoryObject, 29#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 30 seL4_ARM_VCPUObject, 31#endif 32#ifdef CONFIG_ARM_SMMU 33 seL4_ARM_IOPageTableObject, 34#endif 35 seL4_ObjectTypeCount 36} seL4_ArchObjectType; 37 38typedef seL4_Word object_t; 39 40#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT 41#define seL4_ARM_VCPUObject 0xfffe 42#endif 43 44#ifndef CONFIG_ARM_SMMU 45#define seL4_ARM_IOPageTableObject 0xffff 46#endif 47 48#endif /* __ARCH_OBJECTTYPE_H */ 49 50