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 64
10
11block seL4_MessageInfo {
12    field label 52
13    field capsUnwrapped 3
14    field extraCaps 2
15    field length 7
16}
17
18block seL4_CapRights {
19    padding 32
20
21    padding 28
22    field capAllowGrantReply 1
23    field capAllowGrant 1
24    field capAllowRead 1
25    field capAllowWrite 1
26}
27
28-- CNode cap data
29block seL4_CNode_CapData {
30    field guard 58
31    field guardSize 6
32}
33