Preliminary support for small data area in PowerPC port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- cfrontend/Cil2Csyntax.ml 15 additions, 0 deletionscfrontend/Cil2Csyntax.ml
- driver/Clflags.ml 1 addition, 0 deletionsdriver/Clflags.ml
- driver/Driver.ml 5 additions, 0 deletionsdriver/Driver.ml
- extraction/extraction.v 3 additions, 0 deletionsextraction/extraction.v
- powerpc/Asm.v 22 additions, 4 deletionspowerpc/Asm.v
- powerpc/Asmgen.v 5 additions, 2 deletionspowerpc/Asmgen.v
- powerpc/Asmgenproof.v 46 additions, 43 deletionspowerpc/Asmgenproof.v
- powerpc/Asmgenproof1.v 65 additions, 33 deletionspowerpc/Asmgenproof1.v
- powerpc/PrintAsm.ml 39 additions, 14 deletionspowerpc/PrintAsm.ml
Loading
Please register or sign in to comment