source: Deliverables/D3.3/Cminor-experiment/README @ 808

Last change on this file since 808 was 755, checked in by campbell, 10 years ago

An experimental branch of the Cminor semantics.

File size: 835 bytes
1An experimental branch of the Cminor semantics (made from svn revision 754)
2where the statement types are parametrised by an upper bound on the number
3of blocks the statement might exit.  Hence function body statements are
4restricted to zero blocks, ensuring that no St_exit statement can go wrong.
5Similarly, the type of continuations is parametrised by the number of blocks
6contained in the continuation.
8This uncovered a minor anomoly with tail call statements: they used the
9current continuation rather than stripping it back to the last call.
10Offhand I doubt that makes any difference to the semantics, but wasn't
11intended.  (Note that this was only present in my semantics, the prototype
12compiler's interpreter and CompCert were already correct.)
14A reduced prototype of this change is also given in the accompanying Agda
Note: See TracBrowser for help on using the repository browser.