Simplified the treatment of the PowerPC small data area; now more specific to the Diab toolchain.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- cfrontend/Cil2Csyntax.ml 8 additions, 10 deletionscfrontend/Cil2Csyntax.ml
- driver/Clflags.ml 0 additions, 1 deletiondriver/Clflags.ml
- driver/Driver.ml 0 additions, 5 deletionsdriver/Driver.ml
- extraction/extraction.v 0 additions, 1 deletionextraction/extraction.v
- powerpc/Asm.v 9 additions, 7 deletionspowerpc/Asm.v
- powerpc/Asmgen.v 1 addition, 1 deletionpowerpc/Asmgen.v
- powerpc/Asmgenproof.v 42 additions, 45 deletionspowerpc/Asmgenproof.v
- powerpc/Asmgenproof1.v 72 additions, 98 deletionspowerpc/Asmgenproof1.v
- powerpc/PrintAsm.ml 19 additions, 27 deletionspowerpc/PrintAsm.ml
Loading
Please register or sign in to comment