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