source: src/Clight @ 695

Name Size Rev Age Author Last Change
../
cerco 636   10 years campbell A few definitions that will be useful for some preliminary rtlabs …
oldlib 488   10 years campbell Some missing equality constants used by destruct.
test 502   10 years campbell Fix not on nulls on Clight.
acc-0.1.spaces.patch 130.1 KB 416   10 years campbell Fix printing of switch statements as matita terms.
Animation.ma 2.0 KB 693   10 years campbell Separate out whole program executions from the clight semantics and …
AST.ma 15.0 KB 636   10 years campbell A few definitions that will be useful for some preliminary rtlabs …
Cexec.ma 29.5 KB 693   10 years campbell Separate out whole program executions from the clight semantics and …
CexecComplete.ma 16.5 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
CexecEquiv.ma 38.6 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
CexecSound.ma 22.7 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
CostLabel.ma 50 bytes 487   10 years campbell Port Clight semantics to the new-new matita syntax.
Csem.ma 78.3 KB 648   10 years campbell Oops, wrong bitvector negation.
Csyntax.ma 34.0 KB 498   10 years campbell Make block type a little more abstract; remove knowledge about the old …
README 5.5 KB 404   10 years campbell Update C-semantics README.
Note: See TracBrowser for help on using the repository browser.