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