source: src/Clight/test @ 2324

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