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 <mode/types.h>
11 #include <stdint.h>
12 
13 typedef unsigned long word_t;
14 typedef signed long sword_t;
15 /* for printf() formatting */
16 #define _seL4_word_fmt  l
17 
18 typedef word_t vptr_t;
19 typedef word_t paddr_t;
20 typedef word_t pptr_t;
21 typedef word_t cptr_t;
22 typedef word_t node_id_t;
23 typedef word_t cpu_id_t;
24 typedef word_t dom_t;
25 
26 typedef uint8_t  hw_asid_t;
27 
28 enum hwASIDConstants {
29     hwASIDMax = 255,
30     hwASIDBits = 8
31 };
32 
33 /* for libsel4 headers that the kernel shares */
34 typedef word_t seL4_Word;
35 typedef cptr_t seL4_CPtr;
36 typedef uint32_t seL4_Uint32;
37 typedef uint16_t seL4_Uint16;
38 typedef uint8_t seL4_Uint8;
39 typedef node_id_t seL4_NodeId;
40 typedef dom_t seL4_Domain;
41 typedef paddr_t seL4_PAddr;
42 
43 typedef struct kernel_frame {
44     paddr_t paddr;
45     pptr_t pptr;
46     int armExecuteNever;
47     int userAvailable;
48 } kernel_frame_t;
49