source: C-semantics @ 14

Name Size Rev Age Author Last Change
../
binary 10   10 years campbell Add binary arithmetic libraries, use for integers and identifiers (but …
test 12   10 years campbell Make memory model tests more readable. Update README.
AST.ma 13.9 KB 10   10 years campbell Add binary arithmetic libraries, use for integers and identifiers (but …
Cexec.ma 26.4 KB 13   10 years campbell Minor syntactic changes.
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.7 KB 10   10 years campbell Add binary arithmetic libraries, use for integers and identifiers (but …
Csem.ma 59.2 KB 13   10 years campbell Minor syntactic changes.
Csyntax.ma 30.0 KB 4   10 years campbell Some experimental work on executable Clight semantics.
Errors.ma 6.3 KB 4   10 years campbell Some experimental work on executable Clight semantics.
Events.ma 9.0 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
extralib.ma 22.0 KB 14   10 years campbell Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.
Floats.ma 2.6 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Globalenvs.ma 42.6 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Integers.ma 80.2 KB 14   10 years campbell Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.
Maps.ma 42.1 KB 11   10 years campbell Fill in some axioms to aid executablity. Implement global variable …
Mem.ma 122.5 KB 14   10 years campbell Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.
README 4.6 KB 14   10 years campbell Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.
root 32 bytes 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Smallstep.ma 26.7 KB 3   11 years campbell Import work-in-progress port of the CompCert? C semantics to matita.
Values.ma 27.3 KB 14   10 years campbell Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.
Note: See TracBrowser for help on using the repository browser.