

@3254

7 years 
sacerdot 
Code I always forgot to commit.
To be ported to ERTLtoLTLProof.ma.



@3018

7 years 
sacerdot 
1) some files repaired
2) all stuff related to the aborted pass …



@3014

7 years 
tranquil 
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …



@3010

7 years 
tranquil 
same bug as was in liveness is now fixed



@3008

7 years 
tranquil 
corrected bug where the address of pointer calls was not defined as used



@2954

7 years 
tranquil 
resolved circular dependency for ERTLptr's semantics



@2952

7 years 
tranquil 
* corrected all backend premains to not pass any arguments to the …



@2949

7 years 
sacerdot 
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …



@2946

7 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2944

7 years 
sacerdot 
Some progress.



@2942

7 years 
sacerdot 
Many changes:
1. Coloured graphs are now specified in terms of …



@2940

7 years 
sacerdot 
1. StatusSimulationHelper? changed to allow to use status_rel that …



@2938

7 years 
sacerdot 
1. proof of "all eliminable are eliminable" completed
2. the notion of …



@2930

7 years 
sacerdot 
More progress. Some useless parameters have been removed from the …



@2922

7 years 
sacerdot 
Progress: proof of "eliminable statements can be eliminated" almost …



@2898

7 years 
piccolo 
1) simplification of cond and seq case for StatusSimulationHelper? …



@2889

7 years 
sacerdot 
It works very nice!



@2888

7 years 
tranquil 
backtracked some partial changes



@2887

7 years 
tranquil 
Corrected bug where eliminable statements where not eliminated. …



@2883

7 years 
piccolo 
partial commit



@2868

7 years 
sacerdot 
Pretty printing of ERTL and ERTLptr code.



@2863

7 years 
piccolo 
Added new invariant to good_if
Generalized version of cond case for …



@2855

7 years 
piccolo 
little bug fixed in TranslateUtils?.



@2851

7 years 
piccolo 
partial commit



@2849

7 years 
piccolo 
partial commit



@2845

7 years 
piccolo 
ERTLptr to LTL correctness proof started



@2844

7 years 
piccolo 
Stupid bug fixed



@2824

7 years 
tranquil 
* moved sum on lists notation to extranat
* used sum on lists to …



@2819

7 years 
sacerdot 
Proof obligation closed.



@2818

7 years 
sacerdot 
"Repaired", using non computational daemons.



@2808

7 years 
tranquil 
added local_stacksize to joint internal functions to accomodate for …



@2806

7 years 
tranquil 
new b_graph_translate obligations



@2796

7 years 
tranquil 
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …



@2783

7 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2774

7 years 
sacerdot 
1. the compiler now outputs both the stack cost model and the max …



@2741

7 years 
sacerdot 
File used only by untrusted code.
Implemented in Matita to exploit …



@2739

7 years 
sacerdot 
The graph colouring algorithm takes in input also the function.



@2700

7 years 
sacerdot 
1. exponential function dropped in favour of standard library
2. …



@2697

7 years 
sacerdot 
Compiler fixed to include the ERTLptrToLTL pass.



@2694

7 years 
tranquil 
completed ERTLptrToLTL



@2693

7 years 
sacerdot 
1. Stuff moved to correct places.
2. ERTLptr pass added



@2691

7 years 
sacerdot 
ERTLtoERTLptr* moved to the proper place



@2688

7 years 
tranquil 
* in Arithmeticcs.ma: commented include that breaks script in latest …



@2681

7 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2675

7 years 
tranquil 
* a generic graph program transformation



@2674

7 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2666

7 years 
piccolo 
bug fixed in blocks.ma



@2663

7 years 
piccolo 
some minor modifications to ERTLtoERTLptr



@2662

7 years 
piccolo 
Towards a very generalized lemma that summarizes all of Paolo's results.



@2645

7 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2638

7 years 
piccolo 
Backend fixes for last Garnier's commit that removes the regions from …



@2604

7 years 
piccolo 
ERTLtoERTLptr in place.



@2601

7 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2592

7 years 
piccolo 
main lemma of ERTLptr in place



@2590

7 years 
piccolo 
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …



@2570

7 years 
piccolo 
ERTLtoERTLptr in place



@2566

7 years 
piccolo 
ERTL to ERTLptr pass implemented up to a few things to be
left to the …
