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 __LIBSEL4_ARCH_TYPES_H 14#define __LIBSEL4_ARCH_TYPES_H 15 16#include <autoconf.h> 17#include <sel4/simple_types.h> 18#include <sel4/sel4_arch/types.h> 19 20typedef seL4_CPtr seL4_X86_ASIDControl; 21typedef seL4_CPtr seL4_X86_ASIDPool; 22typedef seL4_CPtr seL4_X86_IOSpace; 23typedef seL4_CPtr seL4_X86_IOPort; 24typedef seL4_CPtr seL4_X86_IOPortControl; 25typedef seL4_CPtr seL4_X86_Page; 26typedef seL4_CPtr seL4_X86_PDPT; 27typedef seL4_CPtr seL4_X86_PageDirectory; 28typedef seL4_CPtr seL4_X86_PageTable; 29typedef seL4_CPtr seL4_X86_IOPageTable; 30typedef seL4_CPtr seL4_X86_EPTPML4; 31typedef seL4_CPtr seL4_X86_EPTPDPT; 32typedef seL4_CPtr seL4_X86_EPTPD; 33typedef seL4_CPtr seL4_X86_EPTPT; 34typedef seL4_CPtr seL4_X86_VCPU; 35 36typedef enum { 37 seL4_X86_Default_VMAttributes = 0, 38 seL4_X86_WriteBack = 0, 39 seL4_X86_WriteThrough = 1, 40 seL4_X86_CacheDisabled = 2, 41 seL4_X86_Uncacheable = 3, 42 seL4_X86_WriteCombining = 4, 43 SEL4_FORCE_LONG_ENUM(seL4_X86_VMAttributes), 44} seL4_X86_VMAttributes; 45 46typedef struct seL4_VCPUContext_ { 47 seL4_Word eax, ebx, ecx, edx, esi, edi, ebp; 48} seL4_VCPUContext; 49 50#endif 51