| # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) |
| # |
| # SPDX-License-Identifier: BSD-2-Clause |
| |
| seL4_TCBObject: 10 |
| seL4_EndpointObject: 4 |
| seL4_NotificationObject: 4 |
| seL4_SmallPageObject: 12 |
| seL4_LargePageObject: 16 |
| seL4_ASID_Pool: 12 |
| seL4_ASID_Table: 10 |
| seL4_Slot: 4 |
| seL4_Value_MinUntypedBits: 4 |
| seL4_Value_MaxUntypedBits: 29 |
| seL4_PageTableObject: 10 |
| seL4_PageDirectoryObject: 14 |
| seL4_ARM_SectionObject: 20 |
| seL4_ARM_SuperSectionObject: 24 |
| seL4_IOPageTableObject: 12 |
| seL4_IOPorts: 0 |
| seL4_IODevice: 0 |
| seL4_ARMIODevice: 0 |
| seL4_IRQ: 0 |
| seL4_IOAPICIRQ: 0 |
| seL4_MSIIRQ: 0 |
