source: src/Clight @ 739

Name Size Rev Age Author Last Change
../
cerco 707   9 years campbell Remove old branch, which was merged after the move to src.
test 731   9 years campbell Common definition for animation semantics, and factor out IO definitions.
README 5.5 KB 404   10 years campbell Update C-semantics README.
AST.ma 15.0 KB 738   9 years campbell Use lower case names for identifiers for consistency with CompCert?
CexecComplete.ma 16.6 KB 726   9 years campbell Change identifiers to Words in Clight and RTLabs semantics.
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
CexecSound.ma 23.2 KB 708   9 years campbell Use a more normalize-friendly definition of clight_exec to make the …
Cexec.ma 27.4 KB 731   9 years campbell Common definition for animation semantics, and factor out IO definitions.
Csyntax.ma 34.0 KB 725   9 years campbell Do some light manual disambiguation to make Clight examples go through …
CexecEquiv.ma 39.3 KB 732   9 years campbell Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma
Csem.ma 78.4 KB 725   9 years campbell Do some light manual disambiguation to make Clight examples go through …
acc-0.1.spaces.patch 130.1 KB 416   10 years campbell Fix printing of switch statements as matita terms.
Note: See TracBrowser for help on using the repository browser.