source: src/Clight/test

Name Size Rev Age Author Last Change
../
addptrcharboth.c 315 bytes 2569   7 years campbell Fix Clight semantics for ptr + char. (Compiler works anyway.)
addptrcharboth.c.ma 8.5 KB 2569   7 years campbell Fix Clight semantics for ptr + char. (Compiler works anyway.)
addptrcharboth.test.ma 1.8 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
badconditional.c 173 bytes 2576   7 years campbell Add conditional test case that also uses switch removal.
badconditional.c.ma 2.9 KB 2576   7 years campbell Add conditional test case that also uses switch removal.
badconditional.test.ma 2.0 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
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 …
controlflow.c 538 bytes 2388   7 years campbell Example of each type of control flow statement, plus minor fix to …
controlflow.c.ma 7.5 KB 2391   7 years campbell Revert "Put the post-loop cost label into the Clight while statement …
controlflow.test.ma 2.9 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
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 …
endptr2.c 488 bytes 2395   7 years campbell Proper handling of comparison of pointers off-the-end of an object. We …
endptr2.c.ma 2.7 KB 2395   7 years campbell Proper handling of comparison of pointers off-the-end of an object. We …
endptr2.test.ma 2.7 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
endptr.c 913 bytes 2393   7 years campbell A pointer comparison test case that illustrates a bug.
endptr.c.ma 9.2 KB 2393   7 years campbell A pointer comparison test case that illustrates a bug.
endptr.test.ma 2.8 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
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 …
forcont.c 115 bytes 2407   7 years campbell Sigh, continue in for loops was broken too.
forcont.c.ma 2.0 KB 2407   7 years campbell Sigh, continue in for loops was broken too.
forcont.test.ma 2.9 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
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 2.0 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
implicit.c 104 bytes 2568   7 years campbell Relax some Clight type checks to Cminor type checks to avoid …
implicit.c.ma 2.4 KB 2568   7 years campbell Relax some Clight type checks to Cminor type checks to avoid …
implicit.test.ma 1.8 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
implicitcond.c 105 bytes 2568   7 years campbell Relax some Clight type checks to Cminor type checks to avoid …
implicitcond.c.ma 2.4 KB 2568   7 years campbell Relax some Clight type checks to Cminor type checks to avoid …
implicitcond.test.ma 1.8 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
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 2385   7 years campbell Minor housekeeping.
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.
oneoff.c 56 bytes 2180   7 years campbell Fix off-by-one error in GenMem?.ma.
oneoff.c.ma 1.1 KB 2180   7 years campbell Fix off-by-one error in GenMem?.ma.
oneoff.test.ma 142 bytes 2180   7 years campbell Fix off-by-one error in GenMem?.ma.
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.1 KB 2619   7 years campbell Update some test cases.
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.9 KB 2972   7 years campbell Remove init from a testcase.
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 …
trivial.c 31 bytes 2535   7 years campbell Add the trivial C program with check that there's a measurable subtrace.
trivial.c.ma 561 bytes 2535   7 years campbell Add the trivial C program with check that there's a measurable subtrace.
trivial.test.ma 4.0 KB 2668   7 years campbell Intermediate measurable proof check-in before I change its traces again.
Note: See TracBrowser for help on using the repository browser.