| /* We preprocess this file to extract the sizes of objects for use in camkes/capdl */ |
| #define __ASSEMBLER__ |
| #include <autoconf.h> |
| #include <sel4/constants.h> |
| #include <sel4/sel4_arch/constants.h> |
| #include <sel4/mode/types.h> |
| seL4_TCBObject: seL4_TCBBits |
| seL4_EndpointObject: seL4_EndpointBits |
| seL4_NotificationObject: seL4_NotificationBits |
| seL4_SmallPageObject: seL4_PageBits |
| seL4_LargePageObject: seL4_LargePageBits |
| seL4_ASID_Pool: seL4_ASIDPoolBits |
| seL4_ASID_Table: seL4_ASIDPoolIndexBits |
| seL4_Slot: seL4_SlotBits |
| seL4_Value_MinUntypedBits: seL4_MinUntypedBits |
| seL4_Value_MaxUntypedBits: seL4_MaxUntypedBits |
| seL4_Value_BadgeBits: seL4_BadgeBits |
| #ifdef seL4_ReplyBits |
| seL4_RTReplyObject: seL4_ReplyBits |
| #endif |
| #ifdef seL4_VCPUBits |
| seL4_VCPU: seL4_VCPUBits |
| #endif |
| #ifdef seL4_PageTableBits |
| seL4_PageTableObject: seL4_PageTableBits |
| #endif |
| #ifdef seL4_PageDirBits |
| seL4_PageDirectoryObject: seL4_PageDirBits |
| #endif |
| #ifdef seL4_SectionBits |
| seL4_ARM_SectionObject: seL4_SectionBits |
| #endif |
| #ifdef seL4_SuperSectionBits |
| seL4_ARM_SuperSectionObject: seL4_SuperSectionBits |
| #endif |
| #ifdef seL4_HugePageBits |
| seL4_HugePageObject: seL4_HugePageBits |
| #endif |
| #ifdef seL4_PGDBits |
| seL4_AARCH64_PGD: seL4_PGDBits |
| #endif |
| #ifdef seL4_PUDBits |
| seL4_AARCH64_PUD: seL4_PUDBits |
| #endif |
| #ifdef seL4_IOPageTableBits |
| seL4_IOPageTableObject: seL4_IOPageTableBits |
| #endif |
| #ifdef seL4_PDPTBits |
| seL4_X64_PDPT: seL4_PDPTBits |
| #endif |
| #ifdef seL4_PML4Bits |
| seL4_X64_PML4: seL4_PML4Bits |
| #endif |
| #ifdef seL4_MinSchedContextBits |
| seL4_SchedContextObject: seL4_MinSchedContextBits |
| #endif |
| |
| /* These need not, and should not, be allocated */ |
| seL4_IOPorts: 0 |
| seL4_IODevice: 0 |
| seL4_ARMIODevice: 0 |
| seL4_IRQ: 0 |
| seL4_IOAPICIRQ: 0 |
| seL4_MSIIRQ: 0 |
| seL4_ARMIRQ: 0 |
| seL4_ARMSID: 0 |
| seL4_ARMCB: 0 |