1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#pragma once 8 9#include <config.h> 10#include <assert.h> 11#include <stdint.h> 12 13#if defined(CONFIG_ARCH_IA32) 14compile_assert(long_is_32bits, sizeof(unsigned long) == 4) 15#elif defined(CONFIG_ARCH_X86_64) 16compile_assert(long_is_64bits, sizeof(unsigned long) == 8) 17#endif 18 19typedef unsigned long word_t; 20typedef signed long sword_t; 21typedef word_t vptr_t; 22typedef word_t paddr_t; 23typedef word_t pptr_t; 24typedef word_t cptr_t; 25typedef word_t dev_id_t; 26typedef word_t cpu_id_t; 27typedef uint32_t logical_id_t; 28typedef word_t node_id_t; 29typedef word_t dom_t; 30 31/* for libsel4 headers that the kernel shares */ 32typedef word_t seL4_Word; 33typedef cptr_t seL4_CPtr; 34typedef uint16_t seL4_Uint16; 35typedef uint32_t seL4_Uint32; 36typedef uint8_t seL4_Uint8; 37typedef node_id_t seL4_NodeId; 38typedef paddr_t seL4_PAddr; 39typedef dom_t seL4_Domain; 40 41typedef uint64_t timestamp_t; 42 43