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