|
Last change
on this file since 748 was
739,
checked in by campbell, 10 years ago
|
|
Note on identifiers in CHANGES.
|
|
File size:
1.2 KB
|
| Line | |
|---|
| 1 | 29/03/2011: |
|---|
| 2 | Label moved out of ASM.ma labelled_instruction datatype, as the Paris compiler |
|---|
| 3 | can only produce at most one label per instruction emitted. |
|---|
| 4 | |
|---|
| 5 | Merged the LTL and LIN datatypes. |
|---|
| 6 | |
|---|
| 7 | Added comments to the ASM datatypes. |
|---|
| 8 | |
|---|
| 9 | Changed identifiers from bytes to words. |
|---|
| 10 | |
|---|
| 11 | Formalised missing Assembly.ma file. |
|---|
| 12 | |
|---|
| 13 | 30/03/2011: |
|---|
| 14 | Split translate_statements into two functions. |
|---|
| 15 | |
|---|
| 16 | Added a dependent type for the invariant that a LIN function body does not |
|---|
| 17 | start with a label, and is not empty. |
|---|
| 18 | |
|---|
| 19 | 01/04/2011: |
|---|
| 20 | In retrospect: |
|---|
| 21 | |
|---|
| 22 | The Clight semantics are based on CompCert 1.6 rather than the prototype's; |
|---|
| 23 | this also affects some of the common files. |
|---|
| 24 | |
|---|
| 25 | The identifiers are Words so that we can use BitVectorTries for maps. |
|---|
| 26 | Similarly, integers are based on BitVectors rather than Coq-style binary |
|---|
| 27 | integers + range proof. |
|---|
| 28 | |
|---|
| 29 | 8051 memory spaces are present, but are not (yet?) in the prototype. |
|---|
| 30 | |
|---|
| 31 | Dependent types are used to fix the number of arguments for addressing modes |
|---|
| 32 | in RTLabs. |
|---|
| 33 | |
|---|
| 34 | 04/04/2011: |
|---|
| 35 | common/Identifiers.ma provides identifiers similar to atomSig in the |
|---|
| 36 | prototype, except that we use the universe's name as a tag for the type of |
|---|
| 37 | identifiers to provide some extra type safety. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
