|
|
@2864
|
8 years |
sacerdot |
I must have drunk yesterday: all RTL passes are printed correctly; the …
|
|
|
@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 …
|
|
|
@2856
|
8 years |
sacerdot |
Pretty printing of LTL almost finished.
|
|
|
@2854
|
8 years |
sacerdot |
Pretty printing of the LTL program.
|
|
|
@2834
|
8 years |
sacerdot |
Execution integrated in the compiler, as it was in the prototype. …
|
|
|
@2826
|
8 years |
sacerdot |
New error messages.
|
|
|
@2815
|
8 years |
sacerdot |
exec superseded by exec_all
|
|
|
@2814
|
8 years |
sacerdot |
frontend superseded by execute_all
|
|
|
@2813
|
8 years |
sacerdot |
RTLabs now printed too
|
|
|
@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 …
|
|
|
@2798
|
8 years |
sacerdot |
New error message.
|
|
|
@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.
|
|
|
@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 …
|
|
|
@2776
|
8 years |
sacerdot |
The compiler now extracts 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 …
|
|
|
@2758
|
8 years |
campbell |
Adapt prototype's Clight printer.
Doesn't use cost map yet.
|
|
|
@2747
|
8 years |
sacerdot |
The compiler (frontend + backend)
|
|
|
@2744
|
8 years |
sacerdot |
Build no longer fails.
|
|
|
@2729
|
8 years |
sacerdot |
More errors recognized
|
|
|
@2721
|
8 years |
campbell |
Give the real error in the driver.
|
|
|
@2648
|
8 years |
sacerdot |
Back in sync with the extracted code.
|
|
|
@2636
|
8 years |
campbell |
Extracted front-end.
|
|
|
@2620
|
8 years |
campbell |
Sufficient hacking to run the extracted Clight semantics.
|