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

Name Size Rev Age Author Last Change
../
test 502   10 years campbell Fix not on nulls on Clight.
oldlib 488   10 years campbell Some missing equality constants used by destruct.
cerco 582   10 years campbell Use bit vector operations widely instead of round-trips through Z. …
binary 487   10 years campbell Port Clight semantics to the new-new matita syntax.
Values.ma 29.1 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
SmallstepExec.ma 1.4 KB 469   10 years campbell Update work-in-progress file to match current development.
Smallstep.ma 27.7 KB 535   10 years campbell Minimal integration of bitvectors into Clight semantics - does a …
root 32 bytes 254   10 years campbell Reset matita root.
README 5.5 KB 404   10 years campbell Update C-semantics README.
Mem.ma 114.1 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
Maps.ma 42.2 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
IOMonad.ma 8.2 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
Integers.ma 79.3 KB 582   10 years campbell Use bit vector operations widely instead of round-trips through Z. …
Globalenvs.ma 51.2 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
Floats.ma 2.6 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
extralib.ma 21.7 KB 535   10 years campbell Minimal integration of bitvectors into Clight semantics - does a …
Events.ma 10.6 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
Errors.ma 7.4 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
depends 1.5 KB 474   10 years campbell Reduce "include"s to reduce compilation time. (Will be undone when …
Csyntax.ma 34.0 KB 498   10 years campbell Make block type a little more abstract; remove knowledge about the old …
Csem.ma 77.9 KB 582   10 years campbell Use bit vector operations widely instead of round-trips through Z. …
CostLabel.ma 50 bytes 487   10 years campbell Port Clight semantics to the new-new matita syntax.
Coqlib.ma 31.8 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
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 22.7 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.
CexecComplete.ma 16.5 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
Cexec.ma 30.9 KB 500   10 years campbell Use dependent pointer type to ensure that the representation is always …
AST.ma 15.0 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
Animation.ma 1.9 KB 487   10 years campbell Port Clight semantics to the new-new matita syntax.
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.