source:
C-semantics
@
226
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| 8051-Memory | 157 | 10 years | Make proposed memory spaces semantics more explicit. | ||
| binary | 15 | 11 years | Make some definitions more normalization friendly by a little 'nlet … | ||
| test | 156 | 10 years | pdata support | ||
| root | 32 bytes | 3 | 11 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
| CostLabel.ma | 51 bytes | 177 | 10 years | Missing cost labels file. | |
| SmallstepExec.ma | 1.4 KB | 25 | 10 years | Simplify the IO monad a little. | |
| Floats.ma | 2.6 KB | 3 | 11 years | Import work-in-progress port of the CompCert? C semantics to matita. | |
| README | 4.8 KB | 192 | 10 years | matita rev in README | |
| IOMonad.ma | 6.7 KB | 211 | 10 years | Make io_inject definition more straightforward. | |
| Errors.ma | 7.1 KB | 189 | 10 years | Rework monad notation so that it is displayed well in proof mode. | |
| Events.ma | 9.2 KB | 175 | 10 years | Add cost labels, with the semantics that the label is added to the … | |
| CexecIOcomplete.ma | 11.7 KB | 226 | 10 years | Some incomplete work on completeness of CexecIO wrt Csem. Features … | |
| AST.ma | 14.3 KB | 156 | 10 years | pdata support | |
| compcert-1.7.1-matita.patch | 18.4 KB | 11 | 11 years | Fill in some axioms to aid executablity. Implement global variable … | |
| extralib.ma | 23.9 KB | 181 | 10 years | Sort out some axioms. | |
| Smallstep.ma | 27.8 KB | 20 | 10 years | Add resumption monad based version of the executable semantics with … | |
| Values.ma | 27.9 KB | 156 | 10 years | pdata support | |
| Coqlib.ma | 31.9 KB | 173 | 10 years | Minor changes for newer versions of matita. | |
| Csyntax.ma | 34.2 KB | 175 | 10 years | Add cost labels, with the semantics that the label is added to the … | |
| CexecIO.ma | 39.0 KB | 225 | 10 years | Missing case in cast. | |
| Maps.ma | 42.1 KB | 11 | 11 years | Fill in some axioms to aid executablity. Implement global variable … | |
| Globalenvs.ma | 48.0 KB | 125 | 10 years | Unify memory space / pointer types. Implement global variable … | |
| Csem.ma | 78.3 KB | 226 | 10 years | Some incomplete work on completeness of CexecIO wrt Csem. Features … | |
| Integers.ma | 80.6 KB | 181 | 10 years | Sort out some axioms. | |
| acc-0.1.spaces.patch | 125.6 KB | 160 | 10 years | Patch to acc to parse 8051 memory spaces and output matita terms. | |
| Mem.ma | 127.5 KB | 190 | 10 years | Minor changes to work with current matita HEAD (r10998). | |
Note: See TracBrowser
for help on using the repository browser.
