Timeline
Mar 11, 2013:
- 6:50 PM Changeset [2845] by
- ERTLptr to LTL correctness proof started
- 1:28 PM Changeset [2844] by
- Stupid bug fixed
- 1:02 PM Changeset [2843] by
- 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
- 12:41 PM Changeset [2842] by
- The compiler can now show all back-end traces too (assembly and object …
- 12:40 PM Changeset [2841] by
- The compiler now computes also the stack cost for every intermediate …
- 12:18 PM Changeset [2840] by
- Remove irrelevant stuff from RTLabs_partial_traces
- 12:18 PM Changeset [2839] by
- Basic structure of RTLabs measurable to structured traces results.
Mar 10, 2013:
- 1:21 PM Changeset [2838] by
- Closing some more cases
Mar 9, 2013:
- 12:19 PM Changeset [2837] by
- * filled in evaluation of LTL/LIN's extended instrucitons
Mar 8, 2013:
- 11:55 PM Changeset [2836] by
- …
- 11:54 PM Changeset [2835] by
- Included Uses.ma which is required by the untrusted code. The …
- 11:45 PM Changeset [2834] by
- Execution integrated in the compiler, as it was in the prototype. …
- 11:40 PM Changeset [2833] by
- …
- 11:40 PM Changeset [2832] by
- Added abstraction in front of cases daemon for code extraction.
- 11:38 PM Changeset [2831] by
- …
- 11:37 PM Changeset [2830] by
- Added abstractions in front of cases daemon for code extraction.
- 11:18 PM Changeset [2829] by
- Semantics files committed.
- 11:17 PM Changeset [2828] by
- 1. New semantics.ma file that puts together all semantics. It …
- 9:07 PM Changeset [2827] by
- Everything extracted again.
- 9:07 PM Changeset [2826] by
- New error messages.
- 8:36 PM Changeset [2825] by
- Progress, Clight to Cminor
- 5:37 PM Changeset [2824] by
- * moved sum on lists notation to extranat * used sum on lists to …
- 3:51 PM Changeset [2823] by
- * corrected bug in ERTL semantics (both delframe and newframe did the …
- 12:48 PM Changeset [2822] by
- A consitent proof state for Clight to Cminor, with some progress (and …
- 11:44 AM Changeset [2821] by
- * implemented preclassified system for joint (in joint/joint_fullexec.ma)
- 12:26 AM Changeset [2820] by
- Proof obligation closed.
- 12:14 AM Changeset [2819] by
- Proof obligation closed.
Mar 7, 2013:
- 11:43 PM Changeset [2818] by
- "Repaired", using non computational daemons.
- 10:31 PM Changeset [2817] by
- Repaired after Paolo's commit.
- 10:20 PM Changeset [2816] by
- Repaired after Paolo's commit.
- 9:41 PM Changeset [2815] by
- exec superseded by exec_all
- 9:39 PM Changeset [2814] by
- frontend superseded by execute_all
- 9:34 PM Changeset [2813] by
- RTLabs now printed too
- 9:23 PM Changeset [2812] by
- Pre-classified system for RTLabs.
- 9:22 PM Changeset [2811] by
- Pre-classified system for RTLabs.
- 6:36 PM Changeset [2810] by
- Cminor semantics exported.
- 6:33 PM Changeset [2809] by
- …
- 6:03 PM Changeset [2808] by
- added local_stacksize to joint internal functions to accomodate for …
- 5:43 PM Changeset [2807] by
- Yet another ErrorMessage? Removed corresponding axiom in …
- 2:51 PM Changeset [2806] by
- new b_graph_translate obligations
- 2:01 PM Changeset [2805] by
- Now also prints the trace for the labelled Clight.
- 1:55 PM Changeset [2804] by
- New executable exec_all. It contains a function to run and print all …
- 1:54 PM Changeset [2803] by
- More code extracted, used to debug the compiler.
- 1:53 PM Changeset [2802] by
- New file Clight_classified_system with the classified system for …
- 1:29 PM Changeset [2801] by
- Partial commit not yet finished
- 1:07 PM Changeset [2800] by
- Tidy up Measurable.ma a little, get rid of obsolete comments.
- 1:04 PM Changeset [2799] by
- * added taaf_to_taa, conversion from trace_any_any_free to …
- 12:56 PM Changeset [2798] by
- New error message.
- 12:55 PM Changeset [2797] by
- Extracted again after James's cleanup and the implementation of the …
- 12:10 PM Changeset [2796] by
- * added global notation for existence in Type[1] (\exists[1] x.P) * in …
- 9:31 AM Changeset [2795] by
- Added new function Measurable.observe_all_in_measurable to be used to …
- 7:47 AM Changeset [2794] by
- Minor tweaks/tidying up
Mar 6, 2013:
- 7:23 PM Changeset [2793] by
- Oops, gave fields wrong order during initialisation.
- 4:50 PM Changeset [2792] by
- Make instrumented output a little easier to read.
- 4:50 PM Changeset [2791] by
- Remove dead code in driver.
- 3:48 PM Changeset [2790] by
- Some null handling in conversion from CIL.
- 3:48 PM Changeset [2789] by
- Some changes to the driver to aid debugging.
- 3:48 PM Changeset [2788] by
- Report compiler error
- 3:48 PM Changeset [2787] by
- Output stack costs in driver.
- 2:59 PM Changeset [2786] by
- Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
- 2:58 PM Changeset [2785] by
- Traces.ma repaired
- 2:35 PM Changeset [2784] by
- Repaired after Mauro's commit.
- 12:09 PM Changeset [2783] by
- modified joint_closed_internal_function definition (added condition on …
- 3:03 AM Changeset [2782] by
- 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
- 3:00 AM Changeset [2781] by
- One more computational daemon closed.
- 2:59 AM Changeset [2780] by
- Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
Mar 5, 2013:
- 11:50 PM Changeset [2779] by
- 1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
- 11:34 PM Changeset [2778] by
- Code to pretty-print the IntelHex? output. At the moment the glue code …
- 10:03 PM Changeset [2777] by
- One computational daemon closed.
- 9:53 PM Changeset [2776] by
- The compiler now extracts also the stack cost model.
- 9:52 PM Changeset [2775] by
- The compiler now computes also the stack cost model.
- 6:15 PM Changeset [2774] by
- 1. the compiler now outputs both the stack cost model and the max …
Mar 4, 2013:
- 10:03 AM Changeset [2773] by
- 1. everything extracted again after all bugs in Matita's extraction …
- 9:55 AM Changeset [2772] by
- Useless code removed.
Mar 3, 2013:
- 11:46 PM Changeset [2771] by
- Some speed up in Policy.ma.
- 9:58 PM Changeset [2770] by
- WARNING: another big commit, touching many files in ASM/*.ma This …
- 2:59 PM Changeset [2769] by
- Mistakenly commented out both as_cost_get_label (needed; OK) as well …
- 2:44 PM Changeset [2768] by
- Nightmare: file no longer typechecks, because defn as_cost_get_labels …
- 2:03 PM Changeset [2767] by
- WARNING: BIG commit, which pushes code_size_opt check into …
- 10:39 AM Changeset [2766] by
- pruned redundant dependency on Clight/Cexec?.ma
- 12:23 AM Changeset [2765] by
- 1. correctness.ma repaired 2. we used the OC_preclassified_system to …
Mar 2, 2013:
- 11:59 PM Changeset [2764] by
- preclassified_system for object code
- 11:42 AM Changeset [2763] by
- All daemons in compiler.ma closed (i.e. proof obligations added to the …
- 2:37 AM Changeset [2762] by
- All repaired up to compiler.ma. Note: one daemon is left for one …
- 1:50 AM Changeset [2761] by
- Unused (but not useless) code commented out.
- 1:29 AM Changeset [2760] by
- 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
Mar 1, 2013:
- 7:56 PM Changeset [2759] by
- Print out costs, with choice of style. Note small anti-assertion patch …
- 7:55 PM Changeset [2758] by
- Adapt prototype's Clight printer. Doesn't use cost map yet.
- 7:13 PM Changeset [2757] by
- many things are still broken, but there is a partial backtrack on …
- 1:05 PM Changeset [2756] by
- WARNING: this commit breaks things, sorry, Paolo is going to fix …
- 11:06 AM Changeset [2755] by
- * changed primitives of abstract status (with stuf that is probably …
- 10:26 AM Changeset [2754] by
- 1. WARNING: I commented out one of James's function used in …
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
Note: See TracTimeline
for information about the timeline view.
