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

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