source: src/joint/semanticsUtils.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3265   7 years tranquil added validate_pointer filter in Interference added that intereference …
(edit) @3037   7 years tranquil * ADDRESS joint instruction now has also an offset * corrected call to …
(edit) @2973   7 years tranquil semanticUtils adapted to changes in TranslateUtils?
(edit) @2954   7 years tranquil resolved circular dependency for ERTLptr's semantics
(edit) @2952   7 years tranquil * corrected all back-end premains to not pass any arguments to the …
(edit) @2946   7 years tranquil main novelties: * there is an in-built stack_usage nat in joint …
(edit) @2843   7 years piccolo 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
(edit) @2816   7 years sacerdot Repaired after Paolo's commit.
(edit) @2796   7 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
(edit) @2783   7 years piccolo modified joint_closed_internal_function definition (added condition on …
(edit) @2708   7 years tranquil fixed linearise and LINToASM LINToASM has now correct transformation …
(edit) @2688   7 years tranquil * in Arithmeticcs.ma: commented include that breaks script in latest …
(edit) @2687   7 years tranquil * polished some interfaces
(edit) @2683   7 years tranquil proof of properties of b_graph_program_transform (with an open axiom)
(edit) @2681   7 years tranquil * improvements to the graph translation function * fixed passes up to LTL
(edit) @2675   7 years tranquil * a generic graph program transformation
(edit) @2674   7 years tranquil * another change in block definition * RTLabs -> RTL and ERTL -> …
(edit) @2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
(edit) @2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
(edit) @2529   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
(edit) @2470   7 years tranquil completely separated program counters from code pointers in joint …
(copy) @2457   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
copied from src/joint/SemanticUtils.ma:
(edit) @2443   7 years tranquil changed joint's stack pointer and internal stack
Note: See TracRevisionLog for help on using the revision log.