1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#ifndef __ARCH_TYPES_H 12#define __ARCH_TYPES_H 13 14#include <config.h> 15#include <assert.h> 16#include <stdint.h> 17 18#if defined(CONFIG_ARCH_IA32) 19compile_assert(long_is_32bits, sizeof(unsigned long) == 4) 20#elif defined(CONFIG_ARCH_X86_64) 21compile_assert(long_is_64bits, sizeof(unsigned long) == 8) 22#endif 23 24typedef unsigned long word_t; 25typedef signed long sword_t; 26typedef word_t vptr_t; 27typedef word_t paddr_t; 28typedef word_t pptr_t; 29typedef word_t cptr_t; 30typedef word_t dev_id_t; 31typedef word_t cpu_id_t; 32typedef uint32_t logical_id_t; 33typedef word_t node_id_t; 34typedef word_t dom_t; 35 36/* for libsel4 headers that the kernel shares */ 37typedef word_t seL4_Word; 38typedef cptr_t seL4_CPtr; 39typedef uint16_t seL4_Uint16; 40typedef uint32_t seL4_Uint32; 41typedef uint8_t seL4_Uint8; 42typedef node_id_t seL4_NodeId; 43typedef paddr_t seL4_PAddr; 44typedef dom_t seL4_Domain; 45 46typedef uint64_t timestamp_t; 47#endif 48