source: src/Clight @ 697

Name Size Rev Age Author Last Change
../
cerco 636   9 years campbell A few definitions that will be useful for some preliminary rtlabs …
test 502   9 years campbell Fix not on nulls on Clight.
acc-0.1.spaces.patch 130.1 KB 416   9 years campbell Fix printing of switch statements as matita terms.
Animation.ma 2.0 KB 693   9 years campbell Separate out whole program executions from the clight semantics and …
AST.ma 15.0 KB 636   9 years campbell A few definitions that will be useful for some preliminary rtlabs …
Cexec.ma 29.5 KB 693   9 years campbell Separate out whole program executions from the clight semantics and …
CexecComplete.ma 16.5 KB 500   9 years campbell Use dependent pointer type to ensure that the representation is always …
CexecEquiv.ma 38.6 KB 487   9 years campbell Port Clight semantics to the new-new matita syntax.
CexecSound.ma 22.7 KB 500   9 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   9 years campbell Port Clight semantics to the new-new matita syntax.
Csem.ma 78.3 KB 648   9 years campbell Oops, wrong bitvector negation.
Csyntax.ma 34.0 KB 498   9 years campbell Make block type a little more abstract; remove knowledge about the old …
README 5.5 KB 404   9 years campbell Update C-semantics README.
Note: See TracBrowser for help on using the repository browser.