source:
src/Clight
@
2541
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| cerco | 707 | 10 years | Remove old branch, which was merged after the move to src. | ||
| test | 2535 | 8 years | Add the trivial C program with check that there's a measurable subtrace. | ||
| abstract.ma | 1.5 KB | 2496 | 8 years | Some tentative work on the simulation proof for expressions, in order … | |
| acc-0.1.spaces.patch | 130.1 KB | 416 | 10 years | Fix printing of switch statements as matita terms. | |
| addRuntime.ma | 11.8 KB | 1618 | 9 years | Minor updates due to recent changes. | |
| casts.ma | 7.8 KB | 2032 | 9 years | !! BEWARE: major commit !! 1) [affects everybody] split for … | |
| Cexec.ma | 22.0 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| CexecComplete.ma | 17.4 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| CexecEquiv.ma | 39.8 KB | 2428 | 8 years | Tighten requirements on switch statements in Clight to only give … | |
| CexecInd.ma | 4.6 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| CexecSound.ma | 19.5 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| ClassifyOp.ma | 5.3 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| compcert-1.7.1-matita.patch | 18.4 KB | 11 | 11 years | Fill in some axioms to aid executablity. Implement global variable … | |
| Csem.ma | 51.8 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| Csyntax.ma | 24.9 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| fresh.ma | 4.0 KB | 1629 | 9 years | Sort out most of the fresh names stuff in Clight to Cminor. | |
| frontend_misc.ma | 90.6 KB | 2510 | 8 years | Some progress on the Cl -> Cm front | |
| label.ma | 10.5 KB | 2505 | 8 years | Cleaned up compiler.ma; some refactoring/additional code needed in … | |
| labelSimulation.ma | 54.2 KB | 2487 | 8 years | Set up "after_n_steps" to enforce an invariant on states. | |
| labelSpecification.ma | 1.5 KB | 2319 | 8 years | Generate per-program cost labels rather than per-function ones, and … | |
| memoryInjections.ma | 101.1 KB | 2500 | 8 years | Continuing work on simulation in Clight/Cminor? | |
| MemProperties.ma | 47.8 KB | 2483 | 8 years | Memory injections for Clight to Cminor, partially axiomatized. | |
| README | 5.5 KB | 404 | 10 years | Update C-semantics README. | |
| SimplifyCasts.ma | 147.7 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| switchRemoval.ma | 152.5 KB | 2510 | 8 years | Some progress on the Cl -> Cm front | |
| toCminor.ma | 74.5 KB | 2533 | 8 years | Some fall out from removing floats. | |
| toCminorCorrectness.ma | 40.2 KB | 2527 | 8 years | Progress on CL to CM. | |
| TypeComparison.ma | 6.4 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
Note: See TracBrowser
for help on using the repository browser.
