

@3371

8 years 
piccolo 
Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …



@3265

8 years 
tranquil 
added validate_pointer filter
in Interference added that intereference …



@3263

8 years 
tranquil 
moved callee saved saving and restoring to ERTL > LTL pass (untrusted …



@3262

8 years 
piccolo 
reverted status_simulation_utils



@3261

8 years 
piccolo 
reverted joint_semantics rtl_semantics and ltl_semantics



@3259

8 years 
piccolo 
changed ERTL semantics:
1) added manipulation of stack pointer …



@3154

8 years 
piccolo 
1) changed block_of_call in order to prevent premain calls
2) …



@3145

8 years 
tranquil 
* removed sigma types from traces of intensional events
* completed …



@3118

8 years 
piccolo 
1) finished return case in StatusSimulationHelper?
2) started to write …



@3050

8 years 
piccolo 
1) Added general commutation theorem for monads.
2) Added some …



@3042

8 years 
sacerdot 
Repaired.



@3041

8 years 
sacerdot 
Repaired



@3037

8 years 
tranquil 
* ADDRESS joint instruction now has also an offset
* corrected call to …



@3014

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



@2996

8 years 
sacerdot 
Printing of graphs now starts from the entry point.



@2991

8 years 
piccolo 
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …



@2985

8 years 
sacerdot 
Order of printing of lines in LIN fixed again, truly this time. But I …



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



@2980

8 years 
tranquil 
fixed b_graph_translate



@2973

8 years 
tranquil 
semanticUtils adapted to changes in TranslateUtils?



@2970

8 years 
tranquil 
now joint_if_entry can change when a preamble is added, so code points …



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



@2957

8 years 
tranquil 
fixed semantics_blocks



@2954

8 years 
tranquil 
resolved circular dependency for ERTLptr's semantics



@2952

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



@2950

8 years 
sacerdot 
linearise repaired (did I do the right thing???)



@2946

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



@2940

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



@2939

8 years 
sacerdot 
Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …



@2932

8 years 
sacerdot 
Same comment as previous commit on this file: the previous commit was …



@2929

8 years 
sacerdot 
Bug fixed: the coercion mechanism made you think that the CALL case …



@2920

8 years 
sacerdot 
dos2unixed



@2898

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



@2891

8 years 
piccolo 
added precondition on seq statement and tested correct in the …



@2886

8 years 
piccolo 
partial commit



@2885

8 years 
sacerdot 
Hint at how to change everything.



@2883

8 years 
piccolo 
partial commit



@2879

8 years 
tranquil 
changed coercion from list of joint_seq to blocks to a more efficient one



@2878

8 years 
tranquil 
backtracked some changes that were not ready for commit



@2876

8 years 
tranquil 
corrected another endianess bug in joint_semantics. Switched some …



@2869

8 years 
tranquil 
some reorganization of definitions, and a new taaf_append_taaf



@2865

8 years 
sacerdot 
…



@2863

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



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



@2855

8 years 
piccolo 
little bug fixed in TranslateUtils?.



@2853

8 years 
sacerdot 
Pretty printing of line/label numbers.



@2851

8 years 
piccolo 
partial commit



@2847

8 years 
sacerdot 
…



@2846

8 years 
sacerdot 
Pretty printing of joint programs.



@2843

8 years 
piccolo 
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …



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



@2821

8 years 
tranquil 
* implemented preclassified system for joint (in joint/joint_fullexec.ma)



@2817

8 years 
sacerdot 
Repaired after Paolo's commit.



@2816

8 years 
sacerdot 
Repaired after Paolo's commit.



@2808

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



@2806

8 years 
tranquil 
new b_graph_translate obligations



@2796

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



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



@2774

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



@2760

8 years 
sacerdot 
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …



@2757

8 years 
tranquil 
many things are still broken, but there is a partial backtrack on …



@2755

8 years 
tranquil 
* changed primitives of abstract status (with stuf that is probably …



@2723

8 years 
campbell 
Library name typo fixed.



@2716

8 years 
sacerdot 
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction



@2712

8 years 
tranquil 
changed some fields of joint_internal_function's invariant
fixed linearise



@2708

8 years 
tranquil 
fixed linearise and LINToASM
LINToASM has now correct transformation …



@2702

8 years 
sacerdot 
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …



@2688

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



@2687

8 years 
tranquil 
* polished some interfaces



@2683

8 years 
tranquil 
proof of properties of b_graph_program_transform (with an open axiom)



@2681

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



@2675

8 years 
tranquil 
* a generic graph program transformation



@2674

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



@2666

8 years 
piccolo 
bug fixed in blocks.ma



@2661

8 years 
sacerdot 
stacksize "repaired" by "considering" tailcalls
Some daemons added …



@2655

8 years 
tranquil 
new step in code semantic lemma



@2647

8 years 
sacerdot 
Stupid typo fixed.



@2645

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



@2642

8 years 
piccolo 
fixed joint/Traces after having posed block 0 to be Code



@2641

8 years 
piccolo 
defined dummy block code equals to 0



@2639

8 years 
sacerdot 
We are not going to prove erasure. Thus this becomes dead code.



@2638

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



@2601

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



@2599

8 years 
tranquil 
* map_opt and map on positive maps are now clean (erase empty …



@2595

8 years 
tranquil 
* dropped locals and exit from definition of joint_if_function
* new …



@2592

8 years 
piccolo 
main lemma of ERTLptr in place



@2590

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



@2570

8 years 
piccolo 
ERTLtoERTLptr in place



@2564

8 years 
piccolo 
ERTL fully repaired, useless part of return value of pop_ra
removed.



@2562

8 years 
piccolo 
linearise modified



@2561

8 years 
tranquil 
* moved CALL as different case than joint_seq: lots of broken code now …



@2559

8 years 
piccolo 
lineariseProof finished



@2557

8 years 
tranquil 
minor modification of commented (for now) proof of correctness of …



@2556

8 years 
tranquil 
in joint semantics and traces: added a last popped calling address to …


