source: src/CHANGES @ 816

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

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File size: 1.9 KB
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.
33
3404/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.
38
3908/04/2011:
40  Make return register optional in RTLabs
41
4226/04/2011:
43  Remove register from RTLabs return statements because it ends up being
44  redundant (we always use the register in the function record).
45
46  The constants follow CompCert's rather than the prototype's with the result
47  that they match up more closely with the addressing modes in RTLabs.
48
49  One of the front end operations for subtraction (subpp) appears to be missing
50  from the prototype at present.
51
5219/05/2011:
53  Dump Param var_type from the Clight to Cminor stage - we need to treat them
54  like the other variables.
55
56  Generate list of pointer variables from Clight types rather than
57  recalculation.
58
59  Drop signatures from function call statements in Cminor and RTLabs - they
60  appear to be unused.
Note: See TracBrowser for help on using the repository browser.