Hi David,
are you referring to line 208 in seL4/src/object/objecttype.c?
https://github.com/seL4/seL4/blob/master/src/object/objecttype.c#L208
(As far as I can see, this is the only case in that function that syntactically does not have a return statement).
The procedure recycleCap is indeed not obviously type safe, but it is non-obviously safe ;-)
We prove that “fail” in C never gets called, i.e. in this case that it is impossible for recycleCap to be called with a NullCap. This can be for complex reasons that we would not expect a static analyser to be able to find, although those cases should be rare.
In terms of semantics, fail and halt are left without body, and specified to execute only with precondition “False”.
The actual procedure for proving that fail/halt-statements in C are never called is somewhat roundabout: we prove that the semantic representation of the C program refines the design specification under the assumption that C may do anything it likes wherever there is a “fail” statement in the design specification (including executing statements with precondition False, which is only possible in this trivial sense). We then prove in the design-to-abstract refinement that the design specification never fails. Together this implies that none of the trivial cases occur in C. The reason for this roundabout way is that we did that last step first, before the C proof.
In this specific case, the requirement "cap ~= cap.NullCap” is mentioned in the preconditions of lemma recycle_cap_corres in the design-to-abstract refinement proof:
https://github.com/seL4/l4v/blob/master/proof/refine/Finalise_R.thy#L3877
Cheers,
Gerwin
On 24.01.2015, at 02:27, David Greve