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/
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel