source: src/CHANGES @ 730

Last change on this file since 730 was 730, checked in by campbell, 9 years ago

A few deviations from the prototype / CompCert? that I can think of offhand.

File size: 996 bytes
Line 
129/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
1330/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
1901/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.
Note: See TracBrowser for help on using the repository browser.