|
|
|
@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 …
|
