I ran the sel4 kernel source through the CIL infrastructure front end:

  http://kerneis.github.io/cil/

  CIL reported two warnings:

../../../../seL4/src/object/cnode.c:867: Warning: Body of function isMDBParentOf falls-through. Adding a return statement
../../../../seL4/src/object/objecttype.c:261: Warning: Body of function recycleCap falls-through and cannot find an appropriate return value

  The first warning looks like a weakness in CIL code analysis .. every branch of the condition has a return so the procedure doesn't need a fall-through return.

  The same is not true for the second .. the first branch halt()'s but it doesn't return .. thus the procedure is not "obviously" type safe.

  I'm curious about the this from a reasoning perspective.

  Perhaps the argument is that halt() never terminates (or it "exits"), thus it is OK if the procedure doesn't return a value in that case.  But that argument only works if the logic somehow captures the semantics of halt().

  Are halt() semantics baked into the correctness proofs?  If not, how is this procedure justified?

Thanks,

Dave