source:
Deliverables/D3.1/C-semantics
@
406
Name | Size | Rev | Age | Author | Last Change |
---|---|---|---|---|---|
../ | |||||
binary | 400 | 9 years | Minor changes for the new version of matita. | ||
test | 366 | 9 years | Make I/O type safe, removing a discrepancy between the executable and … | ||
acc-0.1.spaces.patch | 130.0 KB | 292 | 9 years | Update acc 8051 syntax extension patch. Adds memory spaces to Clight … | |
AST.ma | 14.3 KB | 156 | 9 years | pdata support | |
Cexec.ma | 33.0 KB | 400 | 9 years | Minor changes for the new version of matita. | |
CexecComplete.ma | 18.5 KB | 399 | 9 years | Rearrange executable semantics a little. | |
CexecEquiv.ma | 40.8 KB | 399 | 9 years | Rearrange executable semantics a little. | |
CexecSound.ma | 22.7 KB | 399 | 9 years | Rearrange executable semantics a little. | |
compcert-1.7.1-matita.patch | 18.4 KB | 11 | 9 years | Fill in some axioms to aid executablity. Implement global variable … | |
Coqlib.ma | 31.9 KB | 173 | 9 years | Minor changes for newer versions of matita. | |
CostLabel.ma | 51 bytes | 177 | 9 years | Missing cost labels file. | |
Csem.ma | 78.3 KB | 226 | 9 years | Some incomplete work on completeness of CexecIO wrt Csem. Features … | |
Csyntax.ma | 34.2 KB | 255 | 9 years | Really restore matita root. | |
depends | 1.8 KB | 401 | 9 years | Keep a depends file in the repository for the C-semantics. | |
Errors.ma | 7.2 KB | 250 | 9 years | Begin separating soundness from executable semantics. | |
Events.ma | 10.8 KB | 379 | 9 years | More whole execution equivalence - need ability to unfold cofixpoints … | |
extralib.ma | 23.9 KB | 400 | 9 years | Minor changes for the new version of matita. | |
Floats.ma | 2.6 KB | 3 | 10 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
Globalenvs.ma | 48.0 KB | 125 | 9 years | Unify memory space / pointer types. Implement global variable … | |
Integers.ma | 80.6 KB | 181 | 9 years | Sort out some axioms. | |
IOMonad.ma | 8.4 KB | 366 | 9 years | Make I/O type safe, removing a discrepancy between the executable and … | |
Maps.ma | 42.1 KB | 11 | 9 years | Fill in some axioms to aid executablity. Implement global variable … | |
Mem.ma | 127.7 KB | 391 | 9 years | Comment out daemon and its uses - we don't need the properties of the … | |
README | 5.5 KB | 404 | 9 years | Update C-semantics README. | |
root | 32 bytes | 254 | 9 years | Reset matita root. | |
Smallstep.ma | 27.8 KB | 20 | 9 years | Add resumption monad based version of the executable semantics with … | |
SmallstepExec.ma | 1.4 KB | 25 | 9 years | Simplify the IO monad a little. | |
Values.ma | 27.9 KB | 156 | 9 years | pdata support |
Note: See TracBrowser
for help on using the repository browser.