diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 15:35:29 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 15:35:29 +0000 |
commit | 603e931f49ef04188a58895ce38d892511b75b78 (patch) | |
tree | 41f1f2fe83718bf241421c5f185a696d0fab6c7a /arm/CBuiltins.ml | |
parent | 1fe68ad575178f7d8a775906947d2fed94d40976 (diff) | |
download | compcert-603e931f49ef04188a58895ce38d892511b75b78.tar.gz compcert-603e931f49ef04188a58895ce38d892511b75b78.zip |
ARM: added reversed load/store builtins + bswap builtin (to be tested)
IA32: added bswap builtin
Updated Changelog
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/CBuiltins.ml')
-rw-r--r-- | arm/CBuiltins.ml | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index 2e493883..dc4ca60e 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -18,10 +18,24 @@ open Cparser open C -(* No ARM builtins for the moment *) - let builtins = { Builtins.typedefs = []; - Builtins.functions = [] + Builtins.functions = [ + (* Integer arithmetic *) + "__builtin_bswap", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + (* Float arithmetic *) + "__builtin_fsqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* Memory accesses *) + "__builtin_read_int16_reversed", + (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false); + "__builtin_read_int32_reversed", + (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false); + "__builtin_write_int16_reversed", + (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); + "__builtin_write_int32_reversed", + (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); + ] } |