source: Deliverables/D3.1/C-semantics @ 535

Name Size Rev Age Author Last Change
../
binary 487   8 years campbell Port Clight semantics to the new-new matita syntax.
cerco 535   8 years campbell Minimal integration of bitvectors into Clight semantics - does a …
oldlib 488   8 years campbell Some missing equality constants used by destruct.
test 502   8 years campbell Fix not on nulls on Clight.
acc-0.1.spaces.patch 130.1 KB 416   8 years campbell Fix printing of switch statements as matita terms.
Animation.ma 1.9 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
AST.ma 15.0 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
Cexec.ma 30.9 KB 500   8 years campbell Use dependent pointer type to ensure that the representation is always …
CexecComplete.ma 16.5 KB 500   8 years campbell Use dependent pointer type to ensure that the representation is always …
CexecEquiv.ma 38.6 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
CexecSound.ma 22.7 KB 500   8 years campbell Use dependent pointer type to ensure that the representation is always …
compcert-1.7.1-matita.patch 18.4 KB 11   8 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.8 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
CostLabel.ma 50 bytes 487   8 years campbell Port Clight semantics to the new-new matita syntax.
Csem.ma 77.8 KB 502   8 years campbell Fix not on nulls on Clight.
Csyntax.ma 34.0 KB 498   8 years campbell Make block type a little more abstract; remove knowledge about the old …
depends 1.5 KB 474   8 years campbell Reduce "include"s to reduce compilation time. (Will be undone when …
Errors.ma 7.4 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
Events.ma 10.6 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
extralib.ma 21.7 KB 535   8 years campbell Minimal integration of bitvectors into Clight semantics - does a …
Floats.ma 2.6 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
Globalenvs.ma 51.2 KB 500   8 years campbell Use dependent pointer type to ensure that the representation is always …
Integers.ma 79.5 KB 535   8 years campbell Minimal integration of bitvectors into Clight semantics - does a …
IOMonad.ma 8.2 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
Maps.ma 42.2 KB 487   8 years campbell Port Clight semantics to the new-new matita syntax.
Mem.ma 114.1 KB 500   8 years campbell Use dependent pointer type to ensure that the representation is always …
README 5.5 KB 404   8 years campbell Update C-semantics README.
root 32 bytes 254   8 years campbell Reset matita root.
Smallstep.ma 27.7 KB 535   8 years campbell Minimal integration of bitvectors into Clight semantics - does a …
SmallstepExec.ma 1.4 KB 469   8 years campbell Update work-in-progress file to match current development.
Values.ma 29.1 KB 500   8 years campbell Use dependent pointer type to ensure that the representation is always …
Note: See TracBrowser for help on using the repository browser.