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