|
|
@2861
|
8 years |
mckinna |
PROVISIONAL commit:
Unintentional list reversal cause final step of …
|
|
|
@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 …
|
|
|
@2857
|
8 years |
garnier |
CL to CM: some invariants strengthened.
|
|
|
@2856
|
8 years |
sacerdot |
Pretty printing of LTL almost finished.
|
|
|
@2855
|
8 years |
piccolo |
little bug fixed in TranslateUtils?.
|
|
|
@2854
|
8 years |
sacerdot |
Pretty printing of the LTL program.
|
|
|
@2853
|
8 years |
sacerdot |
Pretty printing of line/label numbers.
|
|
|
@2852
|
8 years |
mckinna |
Interim commit to re-establish well-typedness after all the recent …
|
|
|
@2851
|
8 years |
piccolo |
partial commit
|
|
|
@2850
|
8 years |
garnier |
Progress on CL to CM. Some more cases closed modulo some critical …
|
|
|
@2849
|
8 years |
piccolo |
partial commit
|
|
|
@2848
|
8 years |
sacerdot |
The pretty printer for LTL.
|
|
|
@2847
|
8 years |
sacerdot |
…
|
|
|
@2846
|
8 years |
sacerdot |
Pretty printing of joint programs.
|
|
|
@2845
|
8 years |
piccolo |
ERTLptr to LTL correctness proof started
|
|
|
@2844
|
8 years |
piccolo |
Stupid bug fixed
|
|
|
@2843
|
8 years |
piccolo |
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …
|
|
|
@2842
|
8 years |
sacerdot |
The compiler can now show all back-end traces too (assembly and object …
|
|
|
@2841
|
8 years |
sacerdot |
The compiler now computes also the stack cost for every intermediate …
|
|
|
@2840
|
8 years |
campbell |
Remove irrelevant stuff from RTLabs_partial_traces
|
|
|
@2839
|
8 years |
campbell |
Basic structure of RTLabs measurable to structured traces results.
|
|
|
@2838
|
8 years |
garnier |
Closing some more cases
|
|
|
@2837
|
8 years |
tranquil |
* filled in evaluation of LTL/LIN's extended instrucitons
|
|
|
@2836
|
8 years |
sacerdot |
…
|
|
|
@2835
|
8 years |
sacerdot |
Included Uses.ma which is required by the untrusted code.
The …
|
|
|
@2834
|
8 years |
sacerdot |
Execution integrated in the compiler, as it was in the prototype. …
|
|
|
@2833
|
8 years |
sacerdot |
…
|
|
|
@2832
|
8 years |
sacerdot |
Added abstraction in front of cases daemon for code extraction.
|
|
|
@2831
|
8 years |
sacerdot |
…
|
|
|
@2830
|
8 years |
sacerdot |
Added abstractions in front of cases daemon for code extraction.
|
|
|
@2829
|
8 years |
sacerdot |
Semantics files committed.
|
|
|
@2828
|
8 years |
sacerdot |
1. New semantics.ma file that puts together all semantics.
It …
|
|
|
@2827
|
8 years |
sacerdot |
Everything extracted again.
|
|
|
@2826
|
8 years |
sacerdot |
New error messages.
|
|
|
@2825
|
8 years |
garnier |
Progress, Clight to Cminor
|
|
|
@2824
|
8 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
@2823
|
8 years |
tranquil |
* corrected bug in ERTL semantics (both delframe and newframe did the …
|
|
|
@2822
|
8 years |
garnier |
A consitent proof state for Clight to Cminor, with some progress (and …
|
|
|
@2821
|
8 years |
tranquil |
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
|
|
|
@2820
|
8 years |
sacerdot |
Proof obligation closed.
|
|
|
@2819
|
8 years |
sacerdot |
Proof obligation closed.
|
|
|
@2818
|
8 years |
sacerdot |
"Repaired", using non computational daemons.
|
|
|
@2817
|
8 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
@2816
|
8 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
@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
|
|
|
@2812
|
8 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
@2811
|
8 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
@2810
|
8 years |
sacerdot |
Cminor semantics exported.
|
|
|
@2809
|
8 years |
sacerdot |
…
|
|
|
@2808
|
8 years |
tranquil |
added local_stacksize to joint internal functions to accomodate for …
|
|
|
@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 …
|
|
|