source: src/Clight @ 694

Name Size Rev Age Author Last Change
../
binary 487   11 years campbell Port Clight semantics to the new-new matita syntax.
cerco 636   11 years campbell A few definitions that will be useful for some preliminary rtlabs …
oldlib 488   11 years campbell Some missing equality constants used by destruct.
RTLabs 693   11 years campbell Separate out whole program executions from the clight semantics and …
test 502   11 years campbell Fix not on nulls on Clight.
acc-0.1.spaces.patch 130.1 KB 416   11 years campbell Fix printing of switch statements as matita terms.
Animation.ma 2.0 KB 693   11 years campbell Separate out whole program executions from the clight semantics and …
AST.ma 15.0 KB 636   11 years campbell A few definitions that will be useful for some preliminary rtlabs …
Cexec.ma 29.5 KB 693   11 years campbell Separate out whole program executions from the clight semantics and …
CexecComplete.ma 16.5 KB 500   11 years campbell Use dependent pointer type to ensure that the representation is always …
CexecEquiv.ma 38.6 KB 487   11 years campbell Port Clight semantics to the new-new matita syntax.
CexecSound.ma 22.7 KB 500   11 years campbell Use dependent pointer type to ensure that the representation is always …
compcert-1.7.1-matita.patch 18.4 KB 11   11 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.8 KB 487   11 years campbell Port Clight semantics to the new-new matita syntax.
CostLabel.ma 50 bytes 487   11 years campbell Port Clight semantics to the new-new matita syntax.
Csem.ma 78.3 KB 648   11 years campbell Oops, wrong bitvector negation.
Csyntax.ma 34.0 KB 498   11 years campbell Make block type a little more abstract; remove knowledge about the old …
depends 1.5 KB 474   11 years campbell Reduce "include"s to reduce compilation time. (Will be undone when …
Errors.ma 7.4 KB 636   11 years campbell A few definitions that will be useful for some preliminary rtlabs …
Events.ma 10.6 KB 487   11 years campbell Port Clight semantics to the new-new matita syntax.
extralib.ma 21.7 KB 535   11 years campbell Minimal integration of bitvectors into Clight semantics - does a …
Floats.ma 2.6 KB 487   11 years campbell Port Clight semantics to the new-new matita syntax.
FrontEndOps.ma 14.3 KB 639   11 years campbell Preliminary work on RTLabs semantics Will move to somewhere more …
Globalenvs.ma 51.3 KB 583   11 years campbell Abstract pointer offsets a little, similar to the changes for the …
Graphs.ma 635 bytes 639   11 years campbell Preliminary work on RTLabs semantics Will move to somewhere more …
Integers.ma 79.4 KB 648   11 years campbell Oops, wrong bitvector negation.
IOMonad.ma 8.2 KB 487   11 years campbell Port Clight semantics to the new-new matita syntax.
Maps.ma 42.2 KB 487   11 years campbell Port Clight semantics to the new-new matita syntax.
Mem.ma 114.2 KB 583   11 years campbell Abstract pointer offsets a little, similar to the changes for the …
README 5.5 KB 404   11 years campbell Update C-semantics README.
Registers.ma 912 bytes 639   11 years campbell Preliminary work on RTLabs semantics Will move to somewhere more …
root 32 bytes 254   11 years campbell Reset matita root.
Smallstep.ma 27.7 KB 535   11 years campbell Minimal integration of bitvectors into Clight semantics - does a …
SmallstepExec.ma 3.4 KB 693   11 years campbell Separate out whole program executions from the clight semantics and …
Values.ma 34.1 KB 636   11 years campbell A few definitions that will be useful for some preliminary rtlabs …
Note: See TracBrowser for help on using the repository browser.