source: src

Name Size Rev Age Author Last Change
../
ASM 3466   4 years asperti Removed function that is only in the standard library. Maaaany more to …
Clight 3237   4 years campbell Some incomplete work on Clight -> Cminor call steps.
Cminor 3081   5 years campbell Tidy up recent work a little.
common 3259   4 years piccolo changed ERTL semantics: 1) added manipulation of stack pointer …
ERTL 3388   4 years piccolo partial commit
ERTLptr 3254   4 years sacerdot Code I always forgot to commit. To be ported to ERTLtoLTLProof.ma.
joint 3371   4 years piccolo Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …
LIN 3265   4 years tranquil added validate_pointer filter in Interference added that intereference …
LTL 3263   4 years tranquil moved callee saved saving and restoring to ERTL -> LTL pass (untrusted …
RTL 3371   4 years piccolo Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …
RTLabs 3263   4 years tranquil moved callee saved saving and restoring to ERTL -> LTL pass (untrusted …
utilities 3081   5 years campbell Tidy up recent work a little.
acc-matita-printers.patch 7.1 KB 1633   6 years campbell Update Cminor pretty printer and examples.
BACKEND_BROKEN_FILES 713 bytes 2754   5 years sacerdot 1. WARNING: I commented out one of James's function used in …
CHANGES 3.4 KB 1388   6 years sacerdot fetch_result implemented for ERTL. This required a different …
compiler.ma 4.8 KB 3145   5 years tranquil * removed sigma types from traces of intensional events * completed …
correctness.ma 12.6 KB 3156   5 years campbell Rebuild prefix traces in back-end's preferred form.
Makefile 426 bytes 3395   4 years fguidi scan for redundant includes with new version of matitadep
redundant_includes.txt 104 bytes 3395   4 years fguidi scan for redundant includes with new version of matitadep
root 26 bytes 703   7 years sacerdot lib is now the default standard library (after commit 11216 in …
semantics.ma 2.6 KB 3035   5 years mckinna Tweak: tidied up ?/\ldots Conceptual: better monadic threading of …
TODO 606 bytes 1457   6 years sacerdot Bug fixed: when calling an internal function, the pc block is now set …
Note: See TracBrowser for help on using the repository browser.