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