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

../  
ASM  2796  7 years  * added global notation for existence in Type[1] (\exists[1] x.P) * in …  
Clight  2822  7 years  A consitent proof state for Clight to Cminor, with some progress (and …  
Cminor  2809  7 years  …  
common  2824  7 years  * moved sum on lists notation to extranat * used sum on lists to …  
ERTL  2823  7 years  * corrected bug in ERTL semantics (both delframe and newframe did the …  
ERTLptr  2824  7 years  * moved sum on lists notation to extranat * used sum on lists to …  
joint  2824  7 years  * moved sum on lists notation to extranat * used sum on lists to …  
LIN  2783  7 years  modified joint_closed_internal_function definition (added condition on …  
LTL  2796  7 years  * added global notation for existence in Type[1] (\exists[1] x.P) * in …  
RTL  2823  7 years  * corrected bug in ERTL semantics (both delframe and newframe did the …  
RTLabs  2823  7 years  * corrected bug in ERTL semantics (both delframe and newframe did the …  
utilities  2824  7 years  * moved sum on lists notation to extranat * used sum on lists to …  
accmatitaprinters.patch  7.1 KB  1633  9 years  Update Cminor pretty printer and examples.  
BACKEND_BROKEN_FILES  713 bytes  2754  7 years  1. WARNING: I commented out one of James's function used in …  
CHANGES  3.4 KB  1388  9 years  fetch_result implemented for ERTL. This required a different …  
compiler.ma  2.7 KB  2794  7 years  Minor tweaks/tidying up  
correctness.ma  6.5 KB  2802  7 years  New file Clight_classified_system with the classified system for …  
root  26 bytes  703  9 years  lib is now the default standard library (after commit 11216 in …  
TODO  606 bytes  1457  9 years  Bug fixed: when calling an internal function, the pc block is now set … 

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