Timeline
Jan 30, 2013:
- 7:25 PM Changeset [2595] by
- * dropped locals and exit from definition of joint_if_function * new …
Jan 29, 2013:
- 8:28 PM Changeset [2594] by
- Some fixes in memory injections, and some holes filled.
- 12:13 PM Changeset [2593] by
- Finally chased down wicked failure to close case 1.1: of …
- 11:20 AM Changeset [2592] by
- main lemma of ERTLptr in place
Jan 28, 2013:
- 11:43 AM Changeset [2591] by
- Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
Jan 24, 2013:
- 7:52 PM Changeset [2590] by
- added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …
Jan 23, 2013:
- 4:34 PM Changeset [2589] by
- Add one of the simulation diagrams
- 2:38 PM Changeset [2588] by
- modified Cexec/Csem? semantics: . force andbool and orbool types to be …
- 1:51 PM Changeset [2587] by
- Tweak talk a little.
- 1:19 PM Changeset [2586] by
- r
- 12:26 PM Changeset [2585] by
- Many improvements to proof/structured traces talk.
- 5:58 AM Changeset [2584] by
- * Update slides.
Jan 21, 2013:
- 10:58 PM Changeset [2583] by
- Structured traces talk with most of the content; not quite final.
- 11:22 AM HiPEAC13 edited by
- (diff)
- 11:22 AM HiPEAC13 edited by
- (diff)
Jan 15, 2013:
- 3:58 PM Changeset [2582] by
- Some progress on CL to CM.
- 3:45 PM Changeset [2581] by
- commented out back end entirely until knock-on effects of changes to …
- 3:42 PM Changeset [2580] by
- Note on ptr + int vs int + ptr.
- 11:21 AM HiPEAC13 edited by
- (diff)
Jan 14, 2013:
- 1:37 PM Changeset [2579] by
- * First version of Yann's slides.
Jan 11, 2013:
- 9:36 PM Changeset [2578] by
- Progress on CL to CM, fixed some stuff in memory injections.
- 5:05 PM HiPEAC13 edited by
- (diff)
- 5:02 PM HiPEAC13 edited by
- (diff)
- 5:00 PM Changeset [2577] by
- abstract of indexed labels talk
- 4:09 PM WikiStart edited by
- (diff)
- 4:09 PM WikiStart edited by
- (diff)
- 4:08 PM WikiStart edited by
- (diff)
Jan 10, 2013:
- 3:57 PM Changeset [2576] by
- Add conditional test case that also uses switch removal.
Jan 9, 2013:
- 8:51 PM Changeset [2575] by
- temporary commit localised the source of trouble in the proof of …
- 6:33 PM Changeset [2574] by
- Update labelling simulation proofs due to some changes elsewhere.
- 6:15 PM Changeset [2573] by
- temporary fixes to ensure {compiler,correctness}.ma recompile after …
- 1:23 PM Changeset [2572] by
- Progress on toCminorCorrectness.
Jan 8, 2013:
- 5:46 PM Changeset [2571] by
- Lots of little changes for cl_tailcall and classifier change.
Jan 5, 2013:
- 1:41 PM Changeset [2570] by
- ERTLtoERTLptr in place
Jan 4, 2013:
- 2:59 PM Changeset [2569] by
- Fix Clight semantics for ptr + char. (Compiler works anyway.)
- 2:59 PM Changeset [2568] by
- Relax some Clight type checks to Cminor type checks to avoid …
Note: See TracTimeline
for information about the timeline view.
