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