source: C-semantics @ 154

Name Size Rev Age Author Last Change
../
8051-Memory 149   10 years campbell Fill in a few details about 8051 extensions.
binary 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
test 154   10 years campbell Minor test case changes
AST.ma 14.3 KB 153   10 years campbell Use appropriate memory chunks for 8051 pointers.
Cexec.ma 35.4 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
CexecIO.ma 37.2 KB 152   10 years campbell Force whd form for memory during execution
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Coqlib.ma 31.8 KB 24   10 years campbell Separate out IOMonad from the rest of the executable semantics. Start …
Csem.ma 60.3 KB 127   10 years campbell Allow the storage of pointers in suitably large integers.
Csyntax.ma 33.8 KB 153   10 years campbell Use appropriate memory chunks for 8051 pointers.
Errors.ma 6.3 KB 4   10 years campbell Some experimental work on executable Clight semantics.
Events.ma 9.0 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
extralib.ma 22.2 KB 16   10 years campbell Add rest of the expressions to executable Clight semantics.
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Globalenvs.ma 48.0 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Integers.ma 80.5 KB 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
IOMonad.ma 6.1 KB 125   10 years campbell Unify memory space / pointer types. Implement global variable …
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 127.4 KB 153   10 years campbell Use appropriate memory chunks for 8051 pointers.
README 4.6 KB 15   10 years campbell Make some definitions more normalization friendly by a little 'nlet …
root 32 bytes 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
SmallstepExec.ma 1.4 KB 25   10 years campbell Simplify the IO monad a little.
Values.ma 27.8 KB 153   10 years campbell Use appropriate memory chunks for 8051 pointers.
Note: See TracBrowser for help on using the repository browser.