|
|
@2807
|
8 years |
mckinna |
Yet another ErrorMessage?
Removed corresponding axiom in …
|
|
|
@2806
|
8 years |
tranquil |
new b_graph_translate obligations
|
|
|
@2805
|
8 years |
sacerdot |
Now also prints the trace for the labelled Clight.
|
|
|
@2804
|
8 years |
sacerdot |
New executable exec_all. It contains a function to run and print all …
|
|
|
@2803
|
8 years |
sacerdot |
More code extracted, used to debug the compiler.
|
|
|
@2802
|
8 years |
sacerdot |
New file Clight_classified_system with the classified system for …
|
|
|
@2801
|
8 years |
piccolo |
Partial commit not yet finished
|
|
|
@2800
|
8 years |
campbell |
Tidy up Measurable.ma a little, get rid of obsolete comments.
|
|
|
@2799
|
8 years |
tranquil |
* added taaf_to_taa, conversion from trace_any_any_free to …
|
|
|
@2798
|
8 years |
sacerdot |
New error message.
|
|
|
@2797
|
8 years |
sacerdot |
Extracted again after James's cleanup and the implementation of the …
|
|
|
@2796
|
8 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
@2795
|
8 years |
sacerdot |
Added new function Measurable.observe_all_in_measurable to be used to …
|
|
|
@2794
|
8 years |
mckinna |
Minor tweaks/tidying up
|
|
|
@2793
|
8 years |
campbell |
Oops, gave fields wrong order during initialisation.
|
|
|
@2792
|
8 years |
campbell |
Make instrumented output a little easier to read.
|
|
|
@2791
|
8 years |
campbell |
Remove dead code in driver.
|
|
|
@2790
|
8 years |
campbell |
Some null handling in conversion from CIL.
|
|
|
@2789
|
8 years |
campbell |
Some changes to the driver to aid debugging.
|
|
|
@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 …
|
|
|