source:
src/Clight/test
@
2672
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| addptrcharboth.c | 315 bytes | 2569 | 8 years | Fix Clight semantics for ptr + char. (Compiler works anyway.) | |
| addptrcharboth.c.ma | 8.5 KB | 2569 | 8 years | Fix Clight semantics for ptr + char. (Compiler works anyway.) | |
| addptrcharboth.test.ma | 1.8 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| badconditional.c | 173 bytes | 2576 | 8 years | Add conditional test case that also uses switch removal. | |
| badconditional.c.ma | 2.9 KB | 2576 | 8 years | Add conditional test case that also uses switch removal. | |
| badconditional.test.ma | 2.0 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| castremoval.c | 108 bytes | 1198 | 10 years | Clight cast removal (NB: quite different from the prototype). | |
| castremoval.c.ma | 3.5 KB | 1513 | 9 years | Fix up Clight examples. | |
| castremoval.test.ma | 537 bytes | 1876 | 9 years | Update Cexec soundness proof. Change finishes_with predicate to … | |
| controlflow.c | 538 bytes | 2388 | 9 years | Example of each type of control flow statement, plus minor fix to … | |
| controlflow.c.ma | 7.5 KB | 2391 | 9 years | Revert "Put the post-loop cost label into the Clight while statement … | |
| controlflow.test.ma | 2.9 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| duff.c | 1.3 KB | 415 | 10 years | A couple of amusing examples. | |
| duff.c.ma | 22.4 KB | 2176 | 9 years | Remove memory spaces other than XData and Code; simplify pointers as a … | |
| duff.test.ma | 199 bytes | 1876 | 9 years | Update Cexec soundness proof. Change finishes_with predicate to … | |
| endptr2.c | 488 bytes | 2395 | 9 years | Proper handling of comparison of pointers off-the-end of an object. We … | |
| endptr2.c.ma | 2.7 KB | 2395 | 9 years | Proper handling of comparison of pointers off-the-end of an object. We … | |
| endptr2.test.ma | 2.7 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| endptr.c | 913 bytes | 2393 | 9 years | A pointer comparison test case that illustrates a bug. | |
| endptr.c.ma | 9.2 KB | 2393 | 9 years | A pointer comparison test case that illustrates a bug. | |
| endptr.test.ma | 2.8 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| factorial.c | 140 bytes | 415 | 10 years | A couple of amusing examples. | |
| factorial.c.ma | 2.0 KB | 1513 | 9 years | Fix up Clight examples. | |
| factorial.test.ma | 205 bytes | 1876 | 9 years | Update Cexec soundness proof. Change finishes_with predicate to … | |
| forcont.c | 115 bytes | 2407 | 9 years | Sigh, continue in for loops was broken too. | |
| forcont.c.ma | 2.0 KB | 2407 | 9 years | Sigh, continue in for loops was broken too. | |
| forcont.test.ma | 2.9 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| goto-if.c | 74 bytes | 1914 | 9 years | Fix bug in Clight semantics that misses goto-labels inside a cost … | |
| goto-if.c.ma | 856 bytes | 1914 | 9 years | Fix bug in Clight semantics that misses goto-labels inside a cost … | |
| goto-if.test.ma | 2.0 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| implicit.c | 104 bytes | 2568 | 8 years | Relax some Clight type checks to Cminor type checks to avoid … | |
| implicit.c.ma | 2.4 KB | 2568 | 8 years | Relax some Clight type checks to Cminor type checks to avoid … | |
| implicit.test.ma | 1.8 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| implicitcond.c | 105 bytes | 2568 | 8 years | Relax some Clight type checks to Cminor type checks to avoid … | |
| implicitcond.c.ma | 2.4 KB | 2568 | 8 years | Relax some Clight type checks to Cminor type checks to avoid … | |
| implicitcond.test.ma | 1.8 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| insertsort.c | 1016 bytes | 965 | 10 years | Update some Clight examples. | |
| insertsort.c.ma | 17.3 KB | 2176 | 9 years | Remove memory spaces other than XData and Code; simplify pointers as a … | |
| insertsort.test.ma | 2.1 KB | 2385 | 9 years | Minor housekeeping. | |
| io2.c | 91 bytes | 20 | 11 years | Add resumption monad based version of the executable semantics with … | |
| io.c | 75 bytes | 154 | 11 years | Minor test case changes | |
| memorymodel.ma | 3.9 KB | 2176 | 9 years | Remove memory spaces other than XData and Code; simplify pointers as a … | |
| null-local.c | 69 bytes | 458 | 10 years | Add a few more pointer tests. | |
| null-op.c | 235 bytes | 776 | 10 years | Fix up some minor null pointer issues in Clight. Add corresponding … | |
| null-op.c.ma | 3.8 KB | 2176 | 9 years | Remove memory spaces other than XData and Code; simplify pointers as a … | |
| null-op.test.ma | 176 bytes | 1876 | 9 years | Update Cexec soundness proof. Change finishes_with predicate to … | |
| null.c | 111 bytes | 458 | 10 years | Add a few more pointer tests. | |
| oneoff.c | 56 bytes | 2180 | 9 years | Fix off-by-one error in GenMem?.ma. | |
| oneoff.c.ma | 1.1 KB | 2180 | 9 years | Fix off-by-one error in GenMem?.ma. | |
| oneoff.test.ma | 142 bytes | 2180 | 9 years | Fix off-by-one error in GenMem?.ma. | |
| pdata1.c | 172 bytes | 156 | 11 years | pdata support | |
| pdata2.c | 158 bytes | 156 | 11 years | pdata support | |
| ptrbool.c | 173 bytes | 502 | 10 years | Fix not on nulls on Clight. | |
| runtime.c | 106 bytes | 1276 | 10 years | Support for replacing operations with runtime support functions in … | |
| runtime.c.ma | 2.3 KB | 1276 | 10 years | Support for replacing operations with runtime support functions in … | |
| runtime.test.ma | 453 bytes | 1276 | 10 years | Support for replacing operations with runtime support functions in … | |
| search.c | 501 bytes | 717 | 10 years | Clean up Clight examples; better temporary definition of multiply. | |
| search.c.ma | 9.7 KB | 2176 | 9 years | Remove memory spaces other than XData and Code; simplify pointers as a … | |
| search.test.ma | 1.1 KB | 2619 | 8 years | Update some test cases. | |
| spacecadet.c | 113 bytes | 154 | 11 years | Minor test case changes | |
| spaces.c | 1.4 KB | 458 | 10 years | Add a few more pointer tests. | |
| string.c | 130 bytes | 485 | 10 years | Fix treatment of pointers in initialisation data, a little like later … | |
| sum.c | 148 bytes | 758 | 10 years | Implement replacement of global var initialisation data by code in Cminor. | |
| sum.c.ma | 2.6 KB | 2176 | 9 years | Remove memory spaces other than XData and Code; simplify pointers as a … | |
| sum.test.ma | 2.9 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
| switcher.c | 238 bytes | 770 | 10 years | Clight and Cminor examples for switch statement. | |
| switcher.c.ma | 3.6 KB | 1513 | 9 years | Fix up Clight examples. | |
| switcher.test.ma | 1.8 KB | 1883 | 9 years | Ilias' switch removal code, plus a test. | |
| transform1.ma | 3.7 KB | 725 | 10 years | Do some light manual disambiguation to make Clight examples go through … | |
| trivial.c | 31 bytes | 2535 | 8 years | Add the trivial C program with check that there's a measurable subtrace. | |
| trivial.c.ma | 561 bytes | 2535 | 8 years | Add the trivial C program with check that there's a measurable subtrace. | |
| trivial.test.ma | 4.0 KB | 2668 | 8 years | Intermediate measurable proof check-in before I change its traces again. | |
Note: See TracBrowser
for help on using the repository browser.
