

@3265

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



@3037

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



@2973

7 years 
tranquil 
semanticUtils adapted to changes in TranslateUtils?



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



@2946

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



@2843

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



@2816

7 years 
sacerdot 
Repaired after Paolo's commit.



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



@2708

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



@2688

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



@2687

7 years 
tranquil 
* polished some interfaces



@2683

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



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



@2645

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



@2601

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



@2529

7 years 
tranquil 
rewritten function handling in joint
swapped call_rel with ret_rel in …



@2470

7 years 
tranquil 
completely separated program counters from code pointers in joint …



@2457

7 years 
tranquil 
rewritten function handling in joint
swapped call_rel with ret_rel in …


copied from src/joint/SemanticUtils.ma:



@2443

7 years 
tranquil 
changed joint's stack pointer and internal stack
