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/