Timeline
Jul 25, 2011:
- 2:58 PM Changeset [1087] by
- Experimental branch where lookups of local variables in Cminor code …
- 12:41 PM Changeset [1086] by
- Branch for experimenting with identifier binding guarantees.
Jul 21, 2011:
- 5:09 PM Changeset [1085] by
- removed stray files that are no longer needed
- 5:00 PM Changeset [1084] by
- more added on ertl pass: not sure how much should be axiomatised wrt …
- 12:28 PM Changeset [1083] by
- ertl --> ltl statement generation nearly complete. required some …
Jul 20, 2011:
- 5:17 PM Changeset [1082] by
- work from today on ertl -> ltl pass
- 11:26 AM Changeset [1081] by
- completed rtl-ertl pass
Jul 19, 2011:
- 5:28 PM Changeset [1080] by
- more added
- 4:30 PM Changeset [1079] by
- finished rtl to ertl pass modulo conversion of tailcall simplification code
- 12:39 PM Changeset [1078] by
- Implement stack allocation for parameters whose address is taken.
- 12:23 PM Changeset [1077] by
- ack, dependent types are scary
Jul 18, 2011:
- 5:40 PM Changeset [1076] by
- small changes
- 5:21 PM Changeset [1075] by
- nearly completed rtl -> ertl pass removing all option types with dep. types
- 12:44 PM Changeset [1074] by
- - added lookup lemma
Jul 15, 2011:
- 5:38 PM Changeset [1073] by
- more changes from today
- 4:56 PM Changeset [1072] by
- Use not equals form of showing entry/exit labels.
- 2:40 PM Changeset [1071] by
- changes the specific form that the added proofs take to use None, not …
- 12:56 PM Changeset [1070] by
- Show that entry and exit labels are in the RTLabs graph.
- 12:56 PM Changeset [1069] by
- Change odd proof obligation problem back.
Jul 14, 2011:
- 2:27 PM Changeset [1068] by
- rtlabs translation complete subject to axioms
Jul 13, 2011:
- 5:37 PM Changeset [1067] by
- more smaller changes
- 5:12 PM Changeset [1066] by
- changes from today
- 4:02 PM Changeset [1065] by
- Note a couple of deviations from the prototype.
Jul 12, 2011:
- 5:52 PM Changeset [1064] by
- changes from today, nearly complete rtlabs translation pass
Jul 11, 2011:
- 5:52 PM Changeset [1063] by
- changes from today
- 2:09 PM Changeset [1062] by
- separated jmeq and coercions from foldstuff.ma in order to fix the …
Jul 8, 2011:
- 5:49 PM Changeset [1061] by
- more work, bug found, ridiculous map3 function with dep. types added
- 12:17 PM Changeset [1060] by
- work from this morning and yesterday
Jul 6, 2011:
- 6:09 PM Changeset [1059] by
- work from today, bit of a mess at the moment
- 1:29 PM Changeset [1058] by
- Evict CompCert? Maps interface in favour of BitVectorTries?.
Jul 5, 2011:
- 5:53 PM Changeset [1057] by
- changes from today
- 4:25 PM Changeset [1056] by
- Switch to delayed identifier error scheme.
- 12:15 PM Changeset [1055] by
- changes to how identifiers are generated
- 9:51 AM Changeset [1054] by
- - proven policy safe
Jul 4, 2011:
- 6:20 PM Changeset [1053] by
- changes
- 3:31 PM Changeset [1052] by
- removed offsets after reading cerco mailing list
- 1:49 PM Changeset [1051] by
- removed superfluous addressing mode code from RTLabs/syntax.ma
- 10:43 AM Changeset [1050] by
- adding dependent types to map datastructure to remove all option …
Jul 1, 2011:
- 5:45 PM Changeset [1049] by
- more stuff added
- 5:11 PM Changeset [1048] by
- added implementation of haskell associative maps to clean up the mess …
Jun 29, 2011:
- 5:38 PM Changeset [1047] by
- more work from today
- 12:15 PM Changeset [1046] by
- syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
- 10:47 AM Changeset [1045] by
- resolved conflict in rtlabs
Jun 27, 2011:
- 2:17 PM Changeset [1044] by
- - more fold/forall stuff
- 12:28 PM AssemblerFormalisation edited by
- (diff)
- 12:27 PM AssemblerFormalisation edited by
- (diff)
- 12:27 PM AssemblerFormalisation edited by
- (diff)
- 12:26 PM AssemblerFormalisation edited by
- (diff)
- 12:25 PM AssemblerFormalisation edited by
- (diff)
- 12:24 PM AssemblerFormalisation created by
- 12:05 PM WikiStart edited by
- (diff)
Jun 25, 2011:
- 2:32 AM Changeset [1043] by
- Axiom commented out.
- 2:30 AM Changeset [1042] by
- Dead code removed. Slow code uncommented.
Note: See TracTimeline
for information about the timeline view.
