1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4 *
5 * SPDX-License-Identifier: GPL-2.0-only
6 */
7
8#pragma once
9
10
11#include <config.h>
12#include <assert.h>
13#include <stdint.h>
14#include <mode/types.h>
15
16typedef unsigned long word_t;
17typedef signed long sword_t;
18typedef word_t vptr_t;
19typedef word_t paddr_t;
20typedef word_t pptr_t;
21typedef word_t cptr_t;
22typedef word_t dev_id_t;
23typedef word_t cpu_id_t;
24typedef word_t node_id_t;
25typedef word_t dom_t;
26
27/* for libsel4 headers that the kernel shares */
28typedef word_t seL4_Word;
29typedef cptr_t seL4_CPtr;
30typedef uint32_t seL4_Uint32;
31typedef uint8_t seL4_Uint8;
32typedef node_id_t seL4_NodeId;
33typedef paddr_t seL4_PAddr;
34typedef dom_t seL4_Domain;
35
36typedef uint64_t timestamp_t;
37
38#define wordBits BIT(wordRadix)
39
40typedef struct kernel_frame {
41    paddr_t paddr;
42    pptr_t pptr;
43    int userAvailable;
44} kernel_frame_t;
45
46