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