1--
2-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3--
4-- SPDX-License-Identifier: BSD-2-Clause
5--
6
7-- this file contains types shared between libsel4 and the kernel
8
9base 32
10
11block seL4_MessageInfo {
12    field label 20
13    field capsUnwrapped 3
14    field extraCaps 2
15    field length 7
16}
17
18-- Cap rights
19block seL4_CapRights {
20    padding 28
21    field capAllowGrantReply 1
22    field capAllowGrant 1
23    field capAllowRead 1
24    field capAllowWrite 1
25}
26
27-- CNode cap data
28block seL4_CNode_CapData {
29    padding 6
30    field guard 18
31    field guardSize 5
32    padding 3
33}
34