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

Name Size Rev Age Author Last Change
../
binary 487   9 years campbell Port Clight semantics to the new-new matita syntax.
cerco 636   9 years campbell A few definitions that will be useful for some preliminary rtlabs …
oldlib 488   9 years campbell Some missing equality constants used by destruct.
RTLabs 693   9 years campbell Separate out whole program executions from the clight semantics and …
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   9 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.8 KB 487   9 years campbell Port Clight semantics to the new-new matita syntax.
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 …
depends 1.5 KB 474   9 years campbell Reduce "include"s to reduce compilation time. (Will be undone when …
Errors.ma 7.4 KB 636   9 years campbell A few definitions that will be useful for some preliminary rtlabs …
Events.ma 10.6 KB 487   9 years campbell Port Clight semantics to the new-new matita syntax.
extralib.ma 21.7 KB 535   9 years campbell Minimal integration of bitvectors into Clight semantics - does a …
Floats.ma 2.6 KB 487   9 years campbell Port Clight semantics to the new-new matita syntax.
FrontEndOps.ma 14.3 KB 639   9 years campbell Preliminary work on RTLabs semantics Will move to somewhere more …
Globalenvs.ma 51.3 KB 583   9 years campbell Abstract pointer offsets a little, similar to the changes for the …
Graphs.ma 635 bytes 639   9 years campbell Preliminary work on RTLabs semantics Will move to somewhere more …
Integers.ma 79.4 KB 648   9 years campbell Oops, wrong bitvector negation.
IOMonad.ma 8.2 KB 487   9 years campbell Port Clight semantics to the new-new matita syntax.
Maps.ma 42.2 KB 487   9 years campbell Port Clight semantics to the new-new matita syntax.
Mem.ma 114.2 KB 583   9 years campbell Abstract pointer offsets a little, similar to the changes for the …
README 5.5 KB 404   9 years campbell Update C-semantics README.
Registers.ma 912 bytes 639   9 years campbell Preliminary work on RTLabs semantics Will move to somewhere more …
root 32 bytes 254   9 years campbell Reset matita root.
Smallstep.ma 27.7 KB 535   9 years campbell Minimal integration of bitvectors into Clight semantics - does a …
SmallstepExec.ma 3.4 KB 693   9 years campbell Separate out whole program executions from the clight semantics and …
Values.ma 34.1 KB 636   9 years campbell A few definitions that will be useful for some preliminary rtlabs …
Note: See TracBrowser for help on using the repository browser.