Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Revised handling of annotation statements, and more generally built-in ↵ | xleroy | 2011-06-13 | 1 | -15/+14 |
| | | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination). | xleroy | 2011-05-08 | 1 | -0/+126 |
Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |