diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-04-10 15:25:00 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-04-10 15:25:00 +0000 |
commit | 83ca03c1b1f87dc74e0b97c3728c3d8d0c1aad44 (patch) | |
tree | 98334d3f34307f3f7038884995f9c2e662c06d88 /powerpc/CBuiltins.ml | |
parent | a32ed5df6aa31aa5a38a55af9d75880e906721f2 (diff) | |
download | compcert-83ca03c1b1f87dc74e0b97c3728c3d8d0c1aad44.tar.gz compcert-83ca03c1b1f87dc74e0b97c3728c3d8d0c1aad44.zip |
PowerPC:
- added __builtin_trap()
- generate .size and .type directives
- use natural alignment for variables
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1315 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/CBuiltins.ml')
-rw-r--r-- | powerpc/CBuiltins.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 65cd5b4f..da64b565 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -64,6 +64,8 @@ let builtins = { "__builtin_sync", (TVoid [], [], false); "__builtin_isync", + (TVoid [], [], false); + "__builtin_trap", (TVoid [], [], false) ] } |