Timeline
Feb 12, 2013:
- 7:40 PM Changeset [2663] by
- some minor modifications to ERTLtoERTLptr
- 6:56 PM Changeset [2662] by
- Towards a very generalized lemma that summarizes all of Paolo's results.
- 3:26 AM Changeset [2661] by
- stacksize "repaired" by "considering" tailcalls Some daemons added …
- 3:06 AM Changeset [2660] by
- …
- 2:47 AM Changeset [2659] by
- Tailcall elimination no longer necessary: 1. the back-end is almost …
- 2:43 AM Changeset [2658] by
- …
- 2:41 AM Changeset [2657] by
- Cost proof fully repaired. It was broken by the definitions used in …
Feb 11, 2013:
- 6:58 PM Changeset [2656] by
- Ported to tailcalls (currently nothing is classified as a tailcall).
- 4:52 PM Changeset [2655] by
- new step in code semantic lemma
Feb 8, 2013:
- 8:54 PM Changeset [2654] by
- Memory injections in a coherent state.
- 1:45 PM Changeset [2653] by
- …
- 11:49 AM Changeset [2652] by
- String type changed definition.
- 11:13 AM Changeset [2651] by
- Type String changed.
- 8:46 AM Changeset [2650] by
- * Final version of the untrusted software.
Feb 7, 2013:
- 10:43 PM Changeset [2649] by
- …
- 10:43 PM Changeset [2648] by
- Back in sync with the extracted code.
- 10:10 PM Changeset [2647] by
- Stupid typo fixed.
- 9:44 PM Changeset [2646] by
- A tag was classified as an error message. Fixed.
- 9:22 PM Changeset [2645] by
- 1. some broken back-end files repaires, several still to go 2. the …
- 4:42 PM Changeset [2644] by
- Commit some work on FEMeasurable before trying to do something nicer …
- 4:03 PM Changeset [2643] by
- We are not proving erasure, so this is dead code.
- 3:24 PM Changeset [2642] by
- fixed joint/Traces after having posed block 0 to be Code
- 3:15 PM Changeset [2641] by
- defined dummy block code equals to 0
- 3:13 PM Changeset [2640] by
- updated RTL and RTLabs to RTL translation
- 3:07 PM Changeset [2639] by
- We are not going to prove erasure. Thus this becomes dead code.
- 2:15 PM Changeset [2638] by
- Back-end fixes for last Garnier's commit that removes the regions from …
Feb 6, 2013:
- 11:51 PM Changeset [2637] by
- …
- 11:43 PM Changeset [2636] by
- Extracted front-end.
- 11:28 PM Changeset [2635] by
- …
- 11:23 PM Changeset [2634] by
- …
- 11:16 PM Changeset [2633] by
- …
- 11:11 PM Changeset [2632] by
- …
- 10:28 PM Changeset [2631] by
- …
- 10:19 PM Changeset [2630] by
- …
- 10:19 PM Changeset [2629] by
- …
- 10:18 PM Changeset [2628] by
- …
- 10:06 PM Changeset [2627] by
- …
- 9:32 PM Changeset [2626] by
- …
- 8:14 PM Changeset [2625] by
- …
- 6:39 PM Changeset [2624] by
- Properly evict unused and axiomatised Floats.
- 6:39 PM Changeset [2623] by
- Name change update.
- 6:11 PM Changeset [2622] by
- …
- 5:53 PM Changeset [2621] by
- …
- 5:03 PM Changeset [2620] by
- Sufficient hacking to run the extracted Clight semantics.
- 5:03 PM Changeset [2619] by
- Update some test cases.
- 5:03 PM Changeset [2618] by
- Tidy up measurable a little.
- 5:03 PM Changeset [2617] by
- Trivial simplification on split_trace.
- 4:07 PM Changeset [2616] by
- …
- 3:51 PM Changeset [2615] by
- …
- 3:39 PM Changeset [2614] by
- …
- 3:30 PM Changeset [2613] by
- …
- 3:15 PM Changeset [2612] by
- …
- 2:21 PM Changeset [2611] by
- …
- 2:00 PM Changeset [2610] by
- …
- 1:56 PM Changeset [2609] by
- Bibliography in place.
- 1:01 PM Changeset [2608] by
- Regions are no more stored in blocks. block_region now tests the id, …
- 12:15 PM Changeset [2607] by
- authors fixed
- 12:13 PM Changeset [2606] by
- conclusions
- 10:30 AM Changeset [2605] by
- A tentative submission to itp-2013. We will probably not submit the …
Feb 5, 2013:
- 10:49 PM Changeset [2604] by
- ERTLtoERTLptr in place.
- 1:54 PM Changeset [2603] by
- Dead code commented out.
- 1:54 PM Changeset [2602] by
- Dead code commented out.
- 1:36 PM Changeset [2601] by
- Extraction to ocaml is now working, with a couple of bugs left. One …
Feb 1, 2013:
- 12:13 PM Changeset [2600] by
- Memory injections are now only defined relatively to block ids, not …
Jan 31, 2013:
- 5:15 PM Changeset [2599] by
- * map_opt and map on positive maps are now clean (erase empty …
- 12:56 PM Changeset [2598] by
- Tentative, partial draft for the definition of Clight-Cminor …
- 12:07 PM Changeset [2597] by
- Some work in progress on measurable subtrace preservation.
- 12:06 PM Changeset [2596] by
- Use a simpler stack cost map, and then specialise to each semantics.
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.
Note: See TracTimeline
for information about the timeline view.
