source:
src/Clight
@
2125
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| test | 2106 | 7 years | Fix up a couple of proofs broken by recent changes. | ||
| cerco | 707 | 9 years | Remove old branch, which was merged after the move to src. | ||
| TypeComparison.ma | 5.8 KB | 1872 | 8 years | Make binary operations in Cminor/RTLabs properly typed. A few extra … | |
| toCminor.ma | 74.5 KB | 1884 | 8 years | Syntax changes to fit Paolo's commit. | |
| switchRemoval.ma | 40.7 KB | 2076 | 7 years | First steps towards a simulation proof for switch removal. | |
| SimplifyCasts.ma | 153.0 KB | 2103 | 7 years | Make transform_*program take a more general transformation to make … | |
| README | 5.5 KB | 404 | 9 years | Update C-semantics README. | |
| labelSimulation.ma | 56.4 KB | 2118 | 7 years | Labelling preserves behaviour. | |
| label.ma | 7.5 KB | 2103 | 7 years | Make transform_*program take a more general transformation to make … | |
| fresh.ma | 4.0 KB | 1629 | 8 years | Sort out most of the fresh names stuff in Clight to Cminor. | |
| Csyntax.ma | 25.6 KB | 1920 | 8 years | Most of the labelling simulation. Still need to sort out switch … | |
| Csem.ma | 54.1 KB | 2032 | 8 years | !! BEWARE: major commit !! 1) [affects everybody] split for … | |
| compcert-1.7.1-matita.patch | 18.4 KB | 11 | 9 years | Fill in some axioms to aid executablity. Implement global variable … | |
| clightPrintMatita.ml | 15.4 KB | 1633 | 8 years | Update Cminor pretty printer and examples. | |
| ClassifyOp.ma | 6.3 KB | 1872 | 8 years | Make binary operations in Cminor/RTLabs properly typed. A few extra … | |
| CexecSound.ma | 19.4 KB | 2106 | 7 years | Fix up a couple of proofs broken by recent changes. | |
| CexecInd.ma | 4.7 KB | 2019 | 8 years | Split out special induction principle for Clight from soundness file. … | |
| CexecEquiv.ma | 39.7 KB | 1713 | 8 years | Add a distinguished final state to the front-end languages to match up … | |
| CexecComplete.ma | 17.1 KB | 2120 | 7 years | Fix victim of alloc unfolding. | |
| Cexec.ma | 20.6 KB | 2019 | 8 years | Split out special induction principle for Clight from soundness file. … | |
| casts.ma | 7.8 KB | 2032 | 8 years | !! BEWARE: major commit !! 1) [affects everybody] split for … | |
| addRuntime.ma | 11.8 KB | 1618 | 8 years | Minor updates due to recent changes. | |
| acc-0.1.spaces.patch | 130.1 KB | 416 | 9 years | Fix printing of switch statements as matita terms. | |
Note: See TracBrowser
for help on using the repository browser.
