Timeline



Apr 22, 2011:

5:09 PM Changeset [772] by campbell
Implement proper support for RTLabs addressing modes.
3:21 PM Changeset [771] by campbell
Implement switch statements in Cminor -> RTLabs phase
1:49 PM Changeset [770] by campbell
Clight and Cminor examples for switch statement.
1:49 PM Changeset [769] by campbell
Update the Clight matita term printer.
1:49 PM Changeset [768] by campbell
Make Cminor tests test translation to RTLabs.
11:48 AM Changeset [767] by campbell
Use variable shadowing as a poor man's state monad in cminor to rtlabs …

Apr 21, 2011:

7:24 PM Changeset [766] by campbell
Most of the Cminor to RTLabs stage. Is buggy, generates inefficient …

Apr 20, 2011:

5:39 PM Changeset [765] by campbell
Remove superfluous register in RTLabs return statements. Also fix up …
5:38 PM Changeset [764] by campbell
Start Cminor to RTLabs phase. Includes some syntax for matching …
11:33 AM Changeset [763] by mulligan
Changes to RTL-ERTL pass.

Apr 19, 2011:

5:48 PM Changeset [762] by campbell
Make naming of RTLabs files more uniform
3:47 PM RelatedWork edited by campbell
(diff)
3:44 PM RelatedWork edited by campbell
(diff)
3:42 PM RelatedWork edited by campbell
(diff)
2:46 PM RelatedWork edited by mulligan
(diff)
2:46 PM RelatedWork edited by mulligan
(diff)
2:45 PM RelatedWork edited by mulligan
(diff)
2:45 PM RelatedWork edited by mulligan
(diff)
2:40 PM RelatedWork created by mulligan
2:40 PM WikiStart edited by mulligan
(diff)
12:22 PM Changeset [761] by campbell
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
12:22 PM Changeset [760] by campbell
Fix tailcall continuations in Cminor.

Apr 18, 2011:

5:32 PM Changeset [759] by mulligan
More work on the RTL to ERTL pass.
12:33 PM Changeset [758] by campbell
Implement replacement of global var initialisation data by code in Cminor.
12:30 PM Changeset [757] by mulligan
Lots more fixing to get both front and backends using same conventions …

Apr 15, 2011:

5:47 PM Changeset [756] by mulligan
Made a start on RTL. Renaming in ERTL and below to move closer to …
4:26 PM Changeset [755] by campbell
An experimental branch of the Cminor semantics.
1:29 PM Changeset [754] by mulligan
Syntax of RTL.

Apr 14, 2011:

5:54 PM Changeset [753] by mulligan
Work from today.
2:23 PM Changeset [752] by mulligan
Fixed error in BitVectorTrieSet? file.

Apr 13, 2011:

6:52 PM Changeset [751] by campbell
Initial version of the Cminor syntax and semantics.

Apr 12, 2011:

12:32 PM Changeset [750] by campbell
Track some of the changes to the prototype in RTLabs. Just one …
12:32 PM Changeset [749] by campbell
Make definition more explicit to avoid jmeq.
12:32 PM Changeset [748] by campbell
Change example statement for easier testing.

Apr 8, 2011:

2:06 PM Changeset [747] by campbell
Merge the two AST files together (although some definitions still need …
11:51 AM Changeset [746] by mulligan
Changes to bitvectortrieset: equality on sets. Added new file for …
10:15 AM Changeset [745] by mulligan
Changes from yesterday. Slowly implementing the functorized …

Apr 7, 2011:

6:53 PM Changeset [744] by campbell
Evict Coq-style integers from common/Integers.ma. Make more bitvector …
11:11 AM Changeset [743] by mulligan
Removed mess from yesterday.

Apr 6, 2011:

11:16 AM Changeset [742] by mulligan
Added extra debugging feature for Nicolas

Apr 4, 2011:

6:24 PM Changeset [741] by ayache
Bug fix in LINToASM in D2.2's 8051 (negative integers).
5:18 PM Changeset [740] by ayache
New memory model and bug fixes in 8051 branch. Added primitive …
5:16 PM Changeset [739] by campbell
Note on identifiers in CHANGES.
5:13 PM Changeset [738] by campbell
Use lower case names for identifiers for consistency with CompCert?
5:13 PM Changeset [737] by campbell
Use more abstract identifiers in Clight / RTLabs.
5:13 PM Changeset [736] by campbell
Extra type safety for identifiers.

Apr 1, 2011:

6:12 PM Changeset [735] by mulligan
Changes from today
4:14 PM Changeset [734] by mulligan
Fixed lin2asm.
4:09 PM Changeset [733] by mulligan
Fixed partial commit.
2:52 PM Changeset [732] by campbell
Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma
1:35 PM Changeset [731] by campbell
Common definition for animation semantics, and factor out IO definitions.
12:03 PM Changeset [730] by campbell
A few deviations from the prototype / CompCert? that I can think of offhand.
12:03 PM Changeset [729] by campbell
Pretty ugly printer for RTLabs programs.

Mar 31, 2011:

5:53 PM Changeset [728] by mulligan
Changes from last two days.
5:20 PM Changeset [727] by campbell
Enough fixes to let an RTLabs program run.

Mar 30, 2011:

6:47 PM Changeset [726] by campbell
Change identifiers to Words in Clight and RTLabs semantics.
4:16 PM Changeset [725] by campbell
Do some light manual disambiguation to make Clight examples go through …
2:03 PM Changeset [724] by campbell
More tractable version of bitvector_of_nat / nat_of_bitvector.
12:34 PM Changeset [723] by mulligan
Added dependent type internalising the invariant that LIN function …

Mar 29, 2011:

6:32 PM Changeset [722] by mulligan
Committing changes from today. Several files do not typecheck.
6:22 PM Changeset [721] by mulligan
Added diary of changes to project files.
6:21 PM Changeset [720] by campbell
Sort out cost labels.
6:17 PM Changeset [719] by mulligan
Added missing assembly file ported to matita.
5:54 PM Changeset [718] by campbell
Add an AST type (i.e., intermediate language type) for pointers.
5:54 PM Changeset [717] by campbell
Clean up Clight examples; better temporary definition of multiply.
2:29 PM Changeset [716] by mulligan
Finished translating LTL statements to LIN statements. Need to …
1:49 PM Changeset [715] by mulligan
Restored rev from Util as it appears that list reversal is not a part …
12:24 PM Changeset [714] by mulligan
Work on translation from LTL to LIN.
11:48 AM Changeset [713] by mulligan
Commit of initial LTL files.

Mar 28, 2011:

5:40 PM Changeset [712] by mulligan
Changes to get things to typecheck.

Mar 27, 2011:

3:06 PM Changeset [711] by sacerdot

Mar 25, 2011:

6:37 PM Changeset [710] by campbell
Start of way to import RTLabs from prototype compiler.

Mar 23, 2011:

4:39 PM Changeset [709] by sacerdot
Notations should NOT be redefined. Just add a new interpretation.
2:28 PM Changeset [708] by campbell
Use a more normalize-friendly definition of clight_exec to make the …
11:37 AM Changeset [707] by campbell
Remove old branch, which was merged after the move to src.
2:24 AM Changeset [706] by sacerdot
Fixed (reference to basics/pairs was dandling).
2:21 AM Changeset [705] by sacerdot
Ported to new library (notation).
2:19 AM Changeset [704] by sacerdot
Minor speedup in one theorem (less automation).
Note: See TracTimeline for information about the timeline view.