Using the bitfield generator to treat guards and badges as a union type can be convenient, but it requires reserving a bit in the data for the bitfield run time type information. This type information is not needed by the kernel as it knows implicitly whether the passed data is a badge or a guard based on the kind of cap being operated on. However, with the type information present we cannot pass a word sized piece of data to the kernel. The solution here is to go back to using a plain seL4_Word as the type for invocations that want a capdata and let the user either construct a badge as a plain word, or use the seL4_CNode_CapData bitfield for constructing a guard, although they have to manually extract the word representation out of it. |
||
|---|---|---|
| .. | ||
| __init__.py | ||
| bitfield_gen.py | ||
| changed.sh | ||
| invocation_header_gen.py | ||
| sel4_idl.dtd | ||
| syscall_header_gen.py | ||
| syscall_stub_gen.py | ||
| xmllint.sh | ||