| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Use the LGPL instead of the GPL for dual-licensed files | Xavier Leroy | 2021-05-08 | 1 | -4/+5 |
| | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. | ||||
| * | Earlier, more comprehensive check for constant initializers (#88) | Xavier Leroy | 2018-04-26 | 1 | -0/+2 |
| | | | | | | | | | | | | | | | | This commit checks *during elaboration* that initializers for global variables or local static variables are compile-time constants. Before this commit, some non-constant initializers were detected later in the C2C pass, but others were eliminated by the Cleanup pass before being checked, and yet others could cause the Rename pass to abort. To determine which variables are constant l-values, we leverage the recent addition of the Storage_auto storage class and base the determination on the storage class of the identifier: 'auto' or 'register' is not constant, the others are constant. | ||||
| * | Revise parsing of character constants for conformance with ISO C 99. | xleroy | 2013-10-25 | 1 | -0/+1 |
| | | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2352 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
| * | Switching to the new C parser/elaborator/simplifier | xleroy | 2010-03-03 | 1 | -0/+17 |
| git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
 |
index : compcert | |
| CompCert fork with minor modifications for Vericert. |
| aboutsummaryrefslogtreecommitdiffstats |