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 <sel4/objecttype.h>
10#include <sel4/sel4_arch/objecttype.h>
11#include <sel4/arch/objecttype.h>
12
13#define pageType SmallPageObject
14
15enum asidConstants {
16    asidInvalid = 0
17};
18
19#define asidMax (BIT(asidLowBits+asidHighBits)-1)
20
21typedef word_t asid_t;
22
23
24