source: src/Clight/test @ 2176

Name Size Rev Age Author Last Change
../
castremoval.c 108 bytes 1198   8 years campbell Clight cast removal (NB: quite different from the prototype).
castremoval.c.ma 3.5 KB 1513   8 years campbell Fix up Clight examples.
castremoval.test.ma 537 bytes 1876   8 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
duff.c 1.3 KB 415   9 years campbell A couple of amusing examples.
duff.c.ma 22.4 KB 2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
duff.test.ma 199 bytes 1876   8 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
factorial.c 140 bytes 415   9 years campbell A couple of amusing examples.
factorial.c.ma 2.0 KB 1513   8 years campbell Fix up Clight examples.
factorial.test.ma 205 bytes 1876   8 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
goto-if.c 74 bytes 1914   8 years campbell Fix bug in Clight semantics that misses goto-labels inside a cost …
goto-if.c.ma 856 bytes 1914   8 years campbell Fix bug in Clight semantics that misses goto-labels inside a cost …
goto-if.test.ma 1.1 KB 1914   8 years campbell Fix bug in Clight semantics that misses goto-labels inside a cost …
insertsort.c 1016 bytes 965   8 years campbell Update some Clight examples.
insertsort.c.ma 17.3 KB 2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
insertsort.test.ma 2.1 KB 1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
io2.c 91 bytes 20   9 years campbell Add resumption monad based version of the executable semantics with …
io.c 75 bytes 154   9 years campbell Minor test case changes
memorymodel.ma 3.9 KB 2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
null-local.c 69 bytes 458   9 years campbell Add a few more pointer tests.
null-op.c 235 bytes 776   9 years campbell Fix up some minor null pointer issues in Clight. Add corresponding …
null-op.c.ma 3.8 KB 2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
null-op.test.ma 176 bytes 1876   8 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
null.c 111 bytes 458   9 years campbell Add a few more pointer tests.
pdata1.c 172 bytes 156   9 years campbell pdata support
pdata2.c 158 bytes 156   9 years campbell pdata support
ptrbool.c 173 bytes 502   9 years campbell Fix not on nulls on Clight.
runtime.c 106 bytes 1276   8 years campbell Support for replacing operations with runtime support functions in …
runtime.c.ma 2.3 KB 1276   8 years campbell Support for replacing operations with runtime support functions in …
runtime.test.ma 453 bytes 1276   8 years campbell Support for replacing operations with runtime support functions in …
search.c 501 bytes 717   9 years campbell Clean up Clight examples; better temporary definition of multiply.
search.c.ma 9.7 KB 2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
search.test.ma 1.0 KB 2106   7 years campbell Fix up a couple of proofs broken by recent changes.
spacecadet.c 113 bytes 154   9 years campbell Minor test case changes
spaces.c 1.4 KB 458   9 years campbell Add a few more pointer tests.
string.c 130 bytes 485   9 years campbell Fix treatment of pointers in initialisation data, a little like later …
sum.c 148 bytes 758   9 years campbell Implement replacement of global var initialisation data by code in Cminor.
sum.c.ma 2.6 KB 2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
sum.test.ma 2.0 KB 1876   8 years campbell Update Cexec soundness proof. Change finishes_with predicate to …
switcher.c 238 bytes 770   9 years campbell Clight and Cminor examples for switch statement.
switcher.c.ma 3.6 KB 1513   8 years campbell Fix up Clight examples.
switcher.test.ma 1.8 KB 1883   8 years campbell Ilias' switch removal code, plus a test.
transform1.ma 3.7 KB 725   9 years campbell Do some light manual disambiguation to make Clight examples go through …
Note: See TracBrowser for help on using the repository browser.