summaryrefslogtreecommitdiff
path: root/powerpc/extractionMachdep.v
Commit message (Collapse)AuthorAge
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.Gravatar xleroy2014-08-18
| | | | | | | | | | | powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"Gravatar xleroy2013-11-17
| | | | | | | | Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsGravatar xleroy2012-03-07
| | | | | | | | (definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵Gravatar xleroy2012-02-22
| | | | | | as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up handling of linker sections.Gravatar xleroy2010-05-08
| | | | | | | Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM portGravatar xleroy2010-01-25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 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