source:
src
@
2702
Name  Size  Rev  Age  Author  Last Change 

../  
joint  2702  8 years  1. proof closed in ASM/UtilBranch 2. more passes integrated in the …  
ASM  2702  8 years  1. proof closed in ASM/UtilBranch 2. more passes integrated in the …  
Clight  2701  8 years  Automation failure fixed by replacing with hand made proof.  
utilities  2700  8 years  1. exponential function dropped in favour of standard library 2. …  
ERTLptr  2700  8 years  1. exponential function dropped in favour of standard library 2. …  
ERTL  2696  8 years  I can't get this right... :(  
common  2690  8 years  Most of the measurable subtrace preservation proof done.  
RTLabs  2689  8 years  * fixed passes up to linearisation  
RTL  2689  8 years  * fixed passes up to linearisation  
Cminor  2677  8 years  Retain the pointer for the function called in frontend call states so …  
LIN  2645  8 years  1. some broken backend files repaires, several still to go 2. the …  
LTL  2601  8 years  Extraction to ocaml is now working, with a couple of bugs left. One …  
compiler.ma  3.3 KB  2702  8 years  1. proof closed in ASM/UtilBranch 2. more passes integrated in the …  
BACKEND_BROKEN_FILES  575 bytes  2693  8 years  1. Stuff moved to correct places. 2. ERTLptr pass added  
correctness.ma  7.7 KB  2677  8 years  Retain the pointer for the function called in frontend call states so …  
accmatitaprinters.patch  7.1 KB  1633  9 years  Update Cminor pretty printer and examples.  
TODO  606 bytes  1457  9 years  Bug fixed: when calling an internal function, the pc block is now set …  
CHANGES  3.4 KB  1388  9 years  fetch_result implemented for ERTL. This required a different …  
root  26 bytes  703  10 years  lib is now the default standard library (after commit 11216 in … 

Note: See TracBrowser
for help on using the repository browser.