6f3f2579e6
Although the C kernel examines (and may modify) some bits of the message info register, all remaining bits are treated as user data, which the kernel passes through IPC unmodified. The seL4_MessageInfo register describes the message info register. The kernel examines fields `length`, `extraCaps` and `capsUnwrapped`, while the `label` field represents bits available to the user. However, in reality, the user may also use any padding bits for user data, since the kernel also passes these through IPC unmodified. For verification, we would like to phrase specifications in terms of the bitfield definition, and so we would like the `label` field to incorporate all of the bits which the kernel treats as user data. This commit therefore extends the `label` field across the bits which were previously marked as padding. |
||
|---|---|---|
| .. | ||
| arch_include | ||
| include | ||
| mode_include | ||
| sel4_arch_include | ||
| sel4_plat_include | ||
| src | ||
| tools | ||
| CMakeLists.txt | ||
| Kbuild | ||
| Kconfig | ||
| Makefile | ||