summaryrefslogtreecommitdiff
path: root/driver/Driver.ml
Commit message (Collapse)AuthorAge
...
* Revised handling of #pragma section and small data areasGravatar xleroy2010-01-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC/EABI port: preliminary support for #pragma section andGravatar xleroy2009-11-03
| | | | | | | | | | #pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into <arch>/extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified the treatment of the PowerPC small data area; now more specific ↵Gravatar xleroy2009-11-02
| | | | | | to the Diab toolchain. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for small data area in PowerPC port.Gravatar xleroy2009-11-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* No '\n' in Coq strings...Gravatar xleroy2009-08-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:16:39 +0000