source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2788   7 years campbell Report compiler error
(edit) @2787   7 years campbell Output stack costs in driver.
(edit) @2786   7 years piccolo Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
(edit) @2785   7 years piccolo Traces.ma repaired
(edit) @2784   7 years sacerdot Repaired after Mauro's commit.
(edit) @2783   7 years piccolo modified joint_closed_internal_function definition (added condition on …
(edit) @2782   7 years sacerdot 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
(edit) @2781   7 years sacerdot One more computational daemon closed.
(edit) @2780   7 years sacerdot Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
(edit) @2779   7 years sacerdot 1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
(edit) @2778   7 years sacerdot Code to pretty-print the IntelHex? output. At the moment the glue code …
(edit) @2777   7 years sacerdot One computational daemon closed.
(edit) @2776   7 years sacerdot The compiler now extracts also the stack cost model.
(edit) @2775   7 years sacerdot The compiler now computes also the stack cost model.
(edit) @2774   7 years sacerdot 1. the compiler now outputs both the stack cost model and the max …
(edit) @2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
(edit) @2772   7 years sacerdot Useless code removed.
(edit) @2771   7 years sacerdot Some speed up in Policy.ma.
(edit) @2770   7 years mckinna WARNING: another big commit, touching many files in ASM/*.ma This …
(edit) @2769   7 years mckinna Mistakenly commented out both as_cost_get_label (needed; OK) as well …
(edit) @2768   7 years mckinna Nightmare: file no longer typechecks, because defn as_cost_get_labels …
(edit) @2767   7 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
(edit) @2766   7 years mckinna pruned redundant dependency on Clight/Cexec?.ma
(edit) @2765   7 years sacerdot 1. correctness.ma repaired 2. we used the OC_preclassified_system to …
(edit) @2764   7 years sacerdot preclassified_system for object code
(edit) @2763   7 years sacerdot All daemons in compiler.ma closed (i.e. proof obligations added to the …
(edit) @2762   7 years sacerdot All repaired up to compiler.ma. Note: one daemon is left for one …
(edit) @2761   7 years sacerdot Unused (but not useless) code commented out.
(edit) @2760   7 years sacerdot 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
(edit) @2759   7 years campbell Print out costs, with choice of style. Note small anti-assertion patch …
(edit) @2758   7 years campbell Adapt prototype's Clight printer. Doesn't use cost map yet.
(edit) @2757   7 years tranquil many things are still broken, but there is a partial backtrack on …
(edit) @2756   7 years sacerdot WARNING: this commit breaks things, sorry, Paolo is going to fix …
(edit) @2755   7 years tranquil * changed primitives of abstract status (with stuf that is probably …
(edit) @2754   7 years sacerdot 1. WARNING: I commented out one of James's function used in …
(edit) @2753   7 years mckinna Further tidying up thanks to Claudio's strong_decidable intervention; …
(edit) @2752   7 years mckinna Fixed TODO regarding length of list_instr Added ASM/CodeMemory.ma to …
(edit) @2751   7 years mckinna Added | AssemblyTooLarge? : ErrorMessage? to complete compiler.ma
(edit) @2750   7 years mckinna Miscellany on 216 bounds, memory, lemmas+definitions. Completes …
(edit) @2749   7 years regisgia * Updated version of the Frama-C plugin.
(edit) @2748   7 years regisgia * Remove the old version of the plugin.
(edit) @2747   7 years sacerdot The compiler (frontend + backend)
(edit) @2746   7 years sacerdot 1. debugging code in glue 2. updated version
(edit) @2745   7 years sacerdot 1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
(edit) @2744   7 years sacerdot Build no longer fails.
(edit) @2743   7 years sacerdot Latest version of the compiler, extracted with the latest version of …
(edit) @2742   7 years sacerdot Untrusted register colouring fully branched.
(edit) @2741   7 years sacerdot File used only by untrusted code. Implemented in Matita to exploit …
(edit) @2740   7 years sacerdot Graph colouring terminated up to Uses that will be implemented in Matita.
(edit) @2739   7 years sacerdot The graph colouring algorithm takes in input also the function.
(edit) @2738   7 years sacerdot Porting the graph colouring stuff from the untrusted prototype to the …
(edit) @2737   7 years garnier Commit of current proof state for Clight to Cminor translation.
(edit) @2736   7 years sacerdot Untrusted fixpoint computation branched in.
(edit) @2735   7 years campbell Note about loose end in FEMeasurable.
(edit) @2734   7 years mckinna yet another puzzling automation failure, in the repaired case: "" …
(edit) @2733   7 years sacerdot All axioms in set_adt implemented by hand.
(edit) @2732   7 years sacerdot Unused code removed.
(edit) @2731   7 years sacerdot Minimal set of axioms implemented to make the driver run.
(edit) @2730   7 years sacerdot Exported again.
(edit) @2729   7 years sacerdot More errors recognized
(edit) @2728   7 years sacerdot listb.ma => listb_extra.ma for extraction
(edit) @2727   7 years campbell Remove a couple of redundant hypotheses.
(edit) @2726   7 years campbell Show max stack preserved in FEMeasurable.
(edit) @2725   7 years campbell Add observables to FEMeasurable proof; fix silly typo.
(edit) @2724   7 years campbell Add RTLabs cost labelling checks to compiler.ma.
(edit) @2723   7 years campbell Library name typo fixed.
(edit) @2722   7 years campbell It's easier to keep the real function identifier in front-end …
(edit) @2721   7 years campbell Give the real error in the driver.
(edit) @2720   7 years tranquil implemented back end ops that were still axioms
(edit) @2719   7 years sacerdot More values manually abstracted to functions to avoid failwiths at …
(edit) @2718   7 years sacerdot set_empty turned from a value to a function because it is not …
(edit) @2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
(edit) @2716   7 years sacerdot utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
(edit) @2715   7 years sacerdot Policy.ma repaired
(edit) @2714   7 years sacerdot PolicyStep?.ma repaired
(edit) @2713   7 years sacerdot PolicyFront?.ma repaired
(edit) @2712   7 years tranquil changed some fields of joint_internal_function's invariant fixed linearise
(edit) @2711   7 years sacerdot …
(edit) @2710   7 years sacerdot ASMCosts.ma repaired
(edit) @2709   7 years sacerdot LINToAsm repaired
(edit) @2708   7 years tranquil fixed linearise and LINToASM LINToASM has now correct transformation …
(edit) @2707   7 years sacerdot Assembly repaired.
(edit) @2706   7 years mckinna repaired contentious broken automation at end of subgoal 9 of case (* …
(edit) @2705   7 years sacerdot More progress in ASM towards implementing the new pseudoinstructions.
(edit) @2704   7 years tranquil moved JMP from instructions to preinstructions, and added MovSuccessor? …
(edit) @2703   7 years mckinna now includes defn of costlabel_map
(edit) @2702   7 years sacerdot 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
(edit) @2701   7 years sacerdot Automation failure fixed by replacing with hand made proof.
(edit) @2700   7 years sacerdot 1. exponential function dropped in favour of standard library 2. …
(edit) @2699   7 years mckinna simplified dependencies somewhat
(edit) @2698   7 years mckinna simplified dependencies
(edit) @2697   7 years sacerdot Compiler fixed to include the ERTLptrToLTL pass.
(edit) @2696   7 years sacerdot I can't get this right... :-(
(edit) @2695   7 years sacerdot Renamed again.
(edit) @2694   7 years tranquil completed ERTLptrToLTL
(edit) @2693   7 years sacerdot 1. Stuff moved to correct places. 2. ERTLptr pass added
(edit) @2692   7 years garnier Add some more constraints in clight_cminor_data.
(edit) @2691   7 years sacerdot ERTLtoERTLptr* moved to the proper place
(edit) @2690   7 years campbell Most of the measurable subtrace preservation proof done.
(edit) @2689   7 years tranquil * fixed passes up to linearisation
Note: See TracRevisionLog for help on using the revision log.