1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11This module defines the set of kernel object types that are available on all implementations. 12 13> module SEL4.API.Types.Universal where 14 15> import Data.WordLib 16 17\subsection{Types} 18 19\subsubsection{Object Types} 20 21The following is the definition of the five object types that are always available, as well as untyped memory. This enumeration may be extended on some platforms to add platform-specific object types. 22 23> data APIObjectType 24> = Untyped 25> | TCBObject 26> | EndpointObject 27> | NotificationObject 28> | CapTableObject 29> deriving (Enum, Bounded, Eq, Show) 30 31> tcbBlockSizeBits :: Int 32> tcbBlockSizeBits = wordSizeCase 9 11 33 34> epSizeBits :: Int 35> epSizeBits = 4 36 37> ntfnSizeBits :: Int 38> ntfnSizeBits = wordSizeCase 4 5 39 40> cteSizeBits :: Int 41> cteSizeBits = wordSizeCase 4 5 42 43> apiGetObjectSize :: APIObjectType -> Int -> Int 44> apiGetObjectSize Untyped size = size 45> apiGetObjectSize TCBObject _ = tcbBlockSizeBits 46> apiGetObjectSize EndpointObject _ = epSizeBits 47> apiGetObjectSize NotificationObject _ = ntfnSizeBits 48> apiGetObjectSize CapTableObject size = cteSizeBits + size 49 50 51 52