1--
2-- Copyright 2017, Data61
3-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4-- ABN 41 687 119 230.
5--
6-- This software may be distributed and modified according to the terms of
7-- the BSD 2-Clause license. Note that NO WARRANTY is provided.
8-- See "LICENSE_BSD2.txt" for details.
9--
10-- @TAG(DATA61_BSD)
11--
12
13-- this file contains types shared between libsel4 and the kernel
14
15base 64
16
17block seL4_MessageInfo {
18    field label 52
19    field capsUnwrapped 3
20    field extraCaps 2
21    field length 7
22}
23
24block seL4_CapRights {
25    padding 32
26
27    padding 29
28    field capAllowGrant 1
29    field capAllowRead 1
30    field capAllowWrite 1
31}
32
33-- CNode cap data
34block seL4_CNode_CapData {
35    field guard 58
36    field guardSize 6
37}
38