|
|
@2983
|
8 years |
sacerdot |
LIN code was printed in reverse order. But I have not really …
|
|
|
@2982
|
8 years |
sacerdot |
Pretty priting of LIN implemented.
|
|
|
@2981
|
8 years |
sacerdot |
New extraction after code simplification.
|
|
|
@2979
|
8 years |
sacerdot |
1. LINToASM: new extraction (fix deletion backtracked)
2. …
|
|
|
@2977
|
8 years |
sacerdot |
New extraction after several bug fixes.
|
|
|
@2974
|
8 years |
sacerdot |
New extraction.
|
|
|
@2968
|
8 years |
sacerdot |
The initial status memory was not really initialized. Now it is.
|
|
|
@2967
|
8 years |
sacerdot |
Semantics changed so that a terminating joint program that returns an …
|
|
|
@2966
|
8 years |
sacerdot |
Modified by hand files (to improve a little bit the performance).
|
|
|
@2965
|
8 years |
sacerdot |
Code performance improved a bit by hand.
|
|
|
@2963
|
8 years |
sacerdot |
Bug fixed: the pre-main for the final code is now
COST k1
…
|
|
|
@2962
|
8 years |
sacerdot |
Most performant algorithm restored.
|
|
|
@2961
|
8 years |
sacerdot |
Bug fixed (stupid typo in pre-main code made the compiler diverge on …
|
|
|
@2960
|
8 years |
sacerdot |
New extraction, it diverges in RTL execution now.
|
|
|
@2951
|
8 years |
sacerdot |
New extraction. Novely: a pre-main is used in the back-end. …
|
|
|
@2933
|
8 years |
sacerdot |
New extraction, several bug fixed. RTL_semantics fixed by hand, will …
|
|
|
@2921
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2913
|
8 years |
sacerdot |
Bug corrected by hand. It will be corrected automatically by next …
|
|
|
@2910
|
8 years |
sacerdot |
Abstract statuses for ASM and OC completed.
A simple test program can …
|
|
|
@2909
|
8 years |
sacerdot |
New extraction.
|
|
|
@2908
|
8 years |
sacerdot |
Bug fixed by hand, they will be fixed automatically by the new extraction.
|
|
|
@2905
|
8 years |
sacerdot |
Semantics of ASM in place (up to return values and function call …
|
|
|
@2904
|
8 years |
sacerdot |
1. Algorithm modified by hand to make it run faster.
The trusted …
|
|
|
@2903
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2902
|
8 years |
sacerdot |
Quick hack to allow printing of OC code. It will be automatically …
|
|
|
@2890
|
8 years |
sacerdot |
Exported again, now the execution is correct up to LIN for a simple …
|
|
|
@2884
|
8 years |
sacerdot |
Debugging print added.
|
|
|
@2882
|
8 years |
sacerdot |
…
|
|
|
@2881
|
8 years |
sacerdot |
…
|
|
|
@2880
|
8 years |
sacerdot |
…
|
|
|
@2875
|
8 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
@2873
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2868
|
8 years |
sacerdot |
Pretty printing of ERTL and ERTLptr code.
|
|
|
@2867
|
8 years |
sacerdot |
New extraction after indianess bug fixes by Paolo.
|
|
|
@2860
|
8 years |
sacerdot |
RTL printing, core dumps ATM
|
|
|
@2859
|
8 years |
sacerdot |
Pretty printing improved (now it always starts the visit from lbl 1).
|
|
|
@2858
|
8 years |
sacerdot |
Trying to pretty print the code graph in visit order.
Slightly bugged …
|
|
|
@2854
|
8 years |
sacerdot |
Pretty printing of the LTL program.
|
|
|
@2844
|
8 years |
piccolo |
Stupid bug fixed
|
|
|
@2842
|
8 years |
sacerdot |
The compiler can now show all back-end traces too (assembly and object …
|
|
|
@2836
|
8 years |
sacerdot |
…
|
|
|
@2833
|
8 years |
sacerdot |
…
|
|
|
@2831
|
8 years |
sacerdot |
…
|
|
|
@2829
|
8 years |
sacerdot |
Semantics files committed.
|
|
|
@2827
|
8 years |
sacerdot |
Everything extracted again.
|
|
|
@2812
|
8 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
@2810
|
8 years |
sacerdot |
Cminor semantics exported.
|
|
|
@2803
|
8 years |
sacerdot |
More code extracted, used to debug the compiler.
|
|
|
@2797
|
8 years |
sacerdot |
Extracted again after James's cleanup and the implementation of the …
|
|
|
@2789
|
8 years |
campbell |
Some changes to the driver to aid debugging.
|
|
|
@2780
|
8 years |
sacerdot |
Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
|
|
|
@2777
|
8 years |
sacerdot |
One computational daemon closed.
|
|
|
@2775
|
8 years |
sacerdot |
The compiler now computes also the stack cost model.
|
|
|
@2773
|
8 years |
sacerdot |
1. everything extracted again after all bugs in Matita's extraction …
|
|
|
@2759
|
8 years |
campbell |
Print out costs, with choice of style.
Note small anti-assertion patch …
|
|
|
@2746
|
8 years |
sacerdot |
1. debugging code in glue
2. updated version
|
|
|
@2743
|
8 years |
sacerdot |
Latest version of the compiler, extracted with the latest version of …
|
|
|
@2742
|
8 years |
sacerdot |
Untrusted register colouring fully branched.
|
|
|
@2740
|
8 years |
sacerdot |
Graph colouring terminated up to Uses that will be implemented
in Matita.
|
|
|
@2738
|
8 years |
sacerdot |
Porting the graph colouring stuff from the untrusted prototype to the …
|
|
|
@2736
|
8 years |
sacerdot |
Untrusted fixpoint computation branched in.
|
|
|
@2733
|
8 years |
sacerdot |
All axioms in set_adt implemented by hand.
|
|
|
@2731
|
8 years |
sacerdot |
Minimal set of axioms implemented to make the driver run.
|
|
|
@2730
|
8 years |
sacerdot |
Exported again.
|
|
|
@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 …
|
|
|
@2649
|
8 years |
sacerdot |
…
|
|
|
@2636
|
8 years |
campbell |
Extracted front-end.
|
|
|
@2620
|
8 years |
campbell |
Sufficient hacking to run the extracted Clight semantics.
|
|
|
@2602
|
8 years |
piccolo |
Dead code commented out.
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|