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