For consistency, it seems like it'd beneficial if: seL4_RangeError seL4_AlignmentError seL4_DeleteFirst seL4_FailedLookup seL4_RevokeFirst included an indication of which argument the error applies to. For some of these errors, not every call has a unique argument which can cause the erorr. This seems like a relatively straightforward change for me to get acquainted with the full process of modifying and re-verifying the kernel. Are there tradeoffs hidden here that would make this undesirable? -- cmr +16032392210 http://octayn.net/