source:
src/Clight
@
3299
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| cerco | 707 | 10 years | Remove old branch, which was merged after the move to src. | ||
| test | 2972 | 8 years | Remove init from a testcase. | ||
| 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 | 21.9 KB | 2722 | 8 years | It's easier to keep the real function identifier in front-end … | |
| CexecComplete.ma | 17.5 KB | 2722 | 8 years | It's easier to keep the real function identifier in front-end … | |
| CexecEquiv.ma | 39.8 KB | 2677 | 8 years | Retain the pointer for the function called in front-end call states so … | |
| CexecInd.ma | 4.6 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| CexecSound.ma | 20.3 KB | 2722 | 8 years | It's easier to keep the real function identifier in front-end … | |
| ClassifyOp.ma | 5.3 KB | 2468 | 8 years | Floats are gone from the front-end. Some trace amount might remain in … | |
| Clight_abstract.ma | 1.7 KB | 2737 | 8 years | Commit of current proof state for Clight to Cminor translation. | |
| Clight_classified_system.ma | 1.5 KB | 2802 | 8 years | New file Clight_classified_system with the classified system for … | |
| compcert-1.7.1-matita.patch | 18.4 KB | 11 | 11 years | Fill in some axioms to aid executablity. Implement global variable … | |
| Csem.ma | 53.7 KB | 2822 | 8 years | A consitent proof state for Clight to Cminor, with some progress (and … | |
| Csyntax.ma | 24.3 KB | 3178 | 8 years | Some progress on Callstate steps in Clight to Cminor. Note that some … | |
| fresh.ma | 4.0 KB | 1629 | 9 years | Sort out most of the fresh names stuff in Clight to Cminor. | |
| frontend_misc.ma | 109.8 KB | 2822 | 8 years | A consitent proof state for Clight to Cminor, with some progress (and … | |
| label.ma | 11.9 KB | 3030 | 8 years | Break up front-end for correctness proof. Use let rec to prevent … | |
| labelSimulation.ma | 56.1 KB | 3030 | 8 years | Break up front-end for correctness proof. Use let rec to prevent … | |
| labelSpecification.ma | 1.5 KB | 2319 | 9 years | Generate per-program cost labels rather than per-function ones, and … | |
| memoryInjections.ma | 132.5 KB | 3178 | 8 years | Some progress on Callstate steps in Clight to Cminor. Note that some … | |
| MemProperties.ma | 47.9 KB | 2608 | 8 years | Regions are no more stored in blocks. block_region now tests the id, … | |
| README | 5.5 KB | 404 | 10 years | Update C-semantics README. | |
| SimplifyCasts.ma | 147.8 KB | 3049 | 8 years | Globalenvs and initial states for cast simplification. | |
| SimplifyCastsMeasurable.ma | 4.1 KB | 3081 | 8 years | Tidy up recent work a little. | |
| SwitchAndLabel.ma | 8.1 KB | 3081 | 8 years | Tidy up recent work a little. | |
| switchRemoval.ma | 152.1 KB | 3047 | 8 years | Switch removal and labelling combined. | |
| toCminor.ma | 80.6 KB | 3054 | 8 years | Put missing typ check in; adjust proof because I did it a little … | |
| toCminorCorrectness.ma | 153.6 KB | 3237 | 8 years | Some incomplete work on Clight -> Cminor call steps. | |
| toCminorCorrectnessExpr.ma | 111.8 KB | 3176 | 8 years | simplified dependencies | |
| toCminorMeasurable.ma | 6.5 KB | 3178 | 8 years | Some progress on Callstate steps in Clight to Cminor. Note that some … | |
| toCminorOps.ma | 6.4 KB | 3171 | 8 years | removed redundant dependencies | |
| TypeComparison.ma | 6.3 KB | 2645 | 8 years | 1. some broken back-end files repaires, several still to go 2. the … | |
Note: See TracBrowser
for help on using the repository browser.
