An experimental branch of the Cminor semantics (made from svn revision 754)
where the statement types are parametrised by an upper bound on the number
of blocks the statement might exit.  Hence function body statements are
restricted to zero blocks, ensuring that no St_exit statement can go wrong.
Similarly, the type of continuations is parametrised by the number of blocks
contained in the continuation.

This uncovered a minor anomoly with tail call statements: they used the
current continuation rather than stripping it back to the last call.
Offhand I doubt that makes any difference to the semantics, but wasn't
intended.  (Note that this was only present in my semantics, the prototype
compiler's interpreter and CompCert were already correct.)

A reduced prototype of this change is also given in the accompanying Agda
file.