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

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