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