source: src/joint/semanticsUtils.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(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.