Timeline
Feb 28, 2013:
- 5:56 PM Changeset [2753] by
- Further tidying up thanks to Claudio's strong_decidable intervention; …
- 2:36 PM Changeset [2752] by
- Fixed TODO regarding length of list_instr Added ASM/CodeMemory.ma to …
- 2:29 PM Changeset [2751] by
- Added | AssemblyTooLarge? : ErrorMessage? to complete compiler.ma
- 2:27 PM Changeset [2750] by
- Miscellany on 216 bounds, memory, lemmas+definitions. Completes …
- 2:12 PM Changeset [2749] by
- * Updated version of the Frama-C plugin.
- 2:12 PM Changeset [2748] by
- * Remove the old version of the plugin.
Feb 27, 2013:
- 10:48 PM Changeset [2747] by
- The compiler (frontend + backend)
- 10:46 PM Changeset [2746] by
- 1. debugging code in glue 2. updated version
- 10:46 PM Changeset [2745] by
- 1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
- 10:45 PM Changeset [2744] by
- Build no longer fails.
- 9:27 PM Changeset [2743] by
- Latest version of the compiler, extracted with the latest version of …
- 5:42 PM Changeset [2742] by
- Untrusted register colouring fully branched.
- 5:16 PM Changeset [2741] by
- File used only by untrusted code. Implemented in Matita to exploit …
- 4:59 PM Changeset [2740] by
- Graph colouring terminated up to Uses that will be implemented in Matita.
- 4:37 PM Changeset [2739] by
- The graph colouring algorithm takes in input also the function.
- 2:03 PM Changeset [2738] by
- Porting the graph colouring stuff from the untrusted prototype to the …
Feb 26, 2013:
- 7:37 PM Changeset [2737] by
- Commit of current proof state for Clight to Cminor translation.
- 6:18 PM Changeset [2736] by
- Untrusted fixpoint computation branched in.
- 3:35 PM Changeset [2735] by
- Note about loose end in FEMeasurable.
- 3:31 PM Changeset [2734] by
- yet another puzzling automation failure, in the repaired case: "" …
Feb 25, 2013:
- 11:04 PM Changeset [2733] by
- All axioms in set_adt implemented by hand.
- 11:03 PM Changeset [2732] by
- Unused code removed.
- 10:17 PM Changeset [2731] by
- Minimal set of axioms implemented to make the driver run.
- 9:54 PM Changeset [2730] by
- Exported again.
- 9:51 PM Changeset [2729] by
- More errors recognized
- 9:42 PM Changeset [2728] by
- listb.ma => listb_extra.ma for extraction
- 6:43 PM Changeset [2727] by
- Remove a couple of redundant hypotheses.
- 12:11 PM Changeset [2726] by
- Show max stack preserved in FEMeasurable.
- 11:45 AM Changeset [2725] by
- Add observables to FEMeasurable proof; fix silly typo.
Feb 24, 2013:
- 8:39 PM Changeset [2724] by
- Add RTLabs cost labelling checks to compiler.ma.
Feb 23, 2013:
- 5:05 PM Changeset [2723] by
- Library name typo fixed.
- 5:05 PM Changeset [2722] by
- It's easier to keep the real function identifier in front-end …
- 5:05 PM Changeset [2721] by
- Give the real error in the driver.
- 12:03 PM Changeset [2720] by
- implemented back end ops that were still axioms
- 1:29 AM Changeset [2719] by
- More values manually abstracted to functions to avoid failwiths at …
- 1:19 AM Changeset [2718] by
- set_empty turned from a value to a function because it is not …
- 1:16 AM Changeset [2717] by
- Extracted code for the whole compiler. The space cost model is not …
- 1:03 AM Changeset [2716] by
- utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
Feb 22, 2013:
- 11:41 PM Changeset [2715] by
- Policy.ma repaired
- 11:20 PM Changeset [2714] by
- PolicyStep?.ma repaired
- 10:39 PM Changeset [2713] by
- PolicyFront?.ma repaired
- 8:04 PM Changeset [2712] by
- changed some fields of joint_internal_function's invariant fixed linearise
- 7:23 PM Changeset [2711] by
- …
- 7:20 PM Changeset [2710] by
- ASMCosts.ma repaired
- 7:17 PM Changeset [2709] by
- LINToAsm repaired
- 7:11 PM Changeset [2708] by
- fixed linearise and LINToASM LINToASM has now correct transformation …
- 6:45 PM Changeset [2707] by
- Assembly repaired.
- 6:23 PM Changeset [2706] by
- repaired contentious broken automation at end of subgoal 9 of case (* …
- 5:56 PM Changeset [2705] by
- More progress in ASM towards implementing the new pseudoinstructions.
- 3:53 PM Changeset [2704] by
- moved JMP from instructions to preinstructions, and added MovSuccessor? …
- 3:31 PM Changeset [2703] by
- now includes defn of costlabel_map
- 3:27 PM Changeset [2702] by
- 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
- 2:30 PM Changeset [2701] by
- Automation failure fixed by replacing with hand made proof.
- 2:12 PM Changeset [2700] by
- 1. exponential function dropped in favour of standard library 2. …
- 2:11 PM Changeset [2699] by
- simplified dependencies somewhat
- 1:11 PM Changeset [2698] by
- simplified dependencies
- 12:13 PM Changeset [2697] by
- Compiler fixed to include the ERTLptrToLTL pass.
- 12:12 PM Changeset [2696] by
- I can't get this right... :-(
- 12:06 PM Changeset [2695] by
- Renamed again.
- 11:53 AM Changeset [2694] by
- completed ERTLptrToLTL
- 11:39 AM Changeset [2693] by
- 1. Stuff moved to correct places. 2. ERTLptr pass added
- 11:27 AM Changeset [2692] by
- Add some more constraints in clight_cminor_data.
- 11:10 AM Changeset [2691] by
- ERTLtoERTLptr* moved to the proper place
Feb 21, 2013:
- 7:24 PM Changeset [2690] by
- Most of the measurable subtrace preservation proof done.
- 7:23 PM Changeset [2689] by
- * fixed passes up to linearisation
- 6:03 PM Changeset [2688] by
- * in Arithmeticcs.ma: commented include that breaks script in latest …
- 4:20 PM Changeset [2687] by
- * polished some interfaces
- 3:34 PM Changeset [2686] by
- two minor modifications to assist disambiguation of "lookup" file …
- 11:38 AM Changeset [2685] by
- Progress on measurable trace preservation: prefix preserves observable …
- 10:32 AM Changeset [2684] by
- …
Feb 20, 2013:
- 6:41 PM Changeset [2683] by
- proof of properties of b_graph_program_transform (with an open axiom)
Feb 19, 2013:
- 7:24 PM Changeset [2682] by
- Don't apply inv in after_n_steps to last state.
- 6:48 PM Changeset [2681] by
- * improvements to the graph translation function * fixed passes up to LTL
- 4:36 PM Changeset [2680] by
- proofs which previously succeeded fail, thanks to fold on positive_map …
- 3:15 PM Changeset [2679] by
- Further tweak to Brian's changes: no normalization reqd at all!
- 12:23 PM Changeset [2678] by
- Switch to single source step simulations for front-end measurable …
- 12:23 PM Changeset [2677] by
- Retain the pointer for the function called in front-end call states so …
- 12:23 PM Changeset [2676] by
- Less aggressive normalisation in ASMCosts to prevent memory blowup.
Feb 18, 2013:
- 6:26 PM Changeset [2675] by
- * a generic graph program transformation
- 5:48 PM Changeset [2674] by
- * another change in block definition * RTLabs -> RTL and ERTL -> …
- 1:18 PM Changeset [2673] by
- corrected some compilation errors (that might depend on some matita update)
Feb 16, 2013:
- 6:49 PM Changeset [2672] by
- One less axiom on bitvectors.
- 5:12 PM Changeset [2671] by
- simplification
Feb 15, 2013:
- 11:27 AM Changeset [2670] by
- Clean up from recent commits.
- 11:27 AM Changeset [2669] by
- Tweak exec_steps output; show that simulations extend to measurable …
- 11:27 AM Changeset [2668] by
- Intermediate measurable proof check-in before I change its traces again.
Feb 14, 2013:
- 7:10 PM Changeset [2667] by
- Clight to Cminor, statements: some cases down. Subset of the …
- 11:49 AM Changeset [2666] by
- bug fixed in blocks.ma
- 10:01 AM Changeset [2665] by
- …
- 12:01 AM Changeset [2664] by
- Tailcall case implemented (it does not happen ATM).
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
Note: See TracTimeline
for information about the timeline view.
