For consistency, it seems like it'd beneficial if:
seL4_RangeError
seL4_AlignmentError
seL4_DeleteFirst
seL4_FailedLookup
seL4_RevokeFirstincluded 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/
signature.asc
Description: PGP signature
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
