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

Name Size Rev Age Author Last Change
../
binary 400   10 years campbell Minor changes for the new version of matita.
test 458   10 years campbell Add a few more pointer tests.
Floats.ma 2.6 KB 3   10 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
compcert-1.7.1-matita.patch 18.4 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Smallstep.ma 27.8 KB 20   10 years campbell Add resumption monad based version of the executable semantics with …
CostLabel.ma 51 bytes 177   10 years campbell Missing cost labels file.
Integers.ma 80.6 KB 181   10 years campbell Sort out some axioms.
Errors.ma 7.2 KB 250   10 years campbell Begin separating soundness from executable semantics.
root 32 bytes 254   10 years campbell Reset matita root.
Csyntax.ma 34.2 KB 255   10 years campbell Really restore matita root.
Events.ma 10.8 KB 379   10 years campbell More whole execution equivalence - need ability to unfold cofixpoints …
CexecEquiv.ma 40.8 KB 399   10 years campbell Rearrange executable semantics a little.
CexecSound.ma 22.7 KB 399   10 years campbell Rearrange executable semantics a little.
extralib.ma 23.9 KB 400   10 years campbell Minor changes for the new version of matita.
README 5.5 KB 404   10 years campbell Update C-semantics README.
Animation.ma 1.9 KB 409   10 years campbell Update a couple of examples; put support for animation in its own file.
IOMonad.ma 8.5 KB 411   10 years campbell Note associativity of IOMonad, subject to extensionality.
acc-0.1.spaces.patch 130.1 KB 416   10 years campbell Fix printing of switch statements as matita terms.
Mem.ma 127.8 KB 456   10 years campbell Add 24bit initialisation data for null generic pointers.
Values.ma 27.9 KB 456   10 years campbell Add 24bit initialisation data for null generic pointers.
Cexec.ma 33.0 KB 457   10 years campbell Correct checking of function pointers.
Csem.ma 78.7 KB 457   10 years campbell Correct checking of function pointers.
AST.ma 14.3 KB 467   10 years campbell Update some of the commented-out parts of Globalenvs for testing.
Globalenvs.ma 48.1 KB 467   10 years campbell Update some of the commented-out parts of Globalenvs for testing.
CexecComplete.ma 18.5 KB 468   10 years campbell Missing changes to completeness proof for function pointer type fix.
SmallstepExec.ma 1.4 KB 469   10 years campbell Update work-in-progress file to match current development.
Coqlib.ma 31.8 KB 473   10 years campbell Track changes in nlibrary list-theory.ma -> list.ma
depends 1.7 KB 473   10 years campbell Track changes in nlibrary list-theory.ma -> list.ma
Note: See TracBrowser for help on using the repository browser.