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