Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination). | xleroy | 2011-05-08 | 1 | -4/+6 |
| | | | | | | | | | | 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 | ||||
* | Added pass CleanupLabels to remove unreferenced labels in a proved way. | xleroy | 2011-05-08 | 1 | -0/+336 |
ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed. ia32/Asm.v: Pmov_ri can undef flags (if translated to xor) cparser/Ceval.ml: treat ~ in constant exprs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |