diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-09-26 10:51:00 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-09-26 10:51:00 +0200 |
| commit | c42707362b99da19cc7a3f2496d9620dcc0dfa62 (patch) | |
| tree | 51482a67e86f3130b1cb3067c34c7b5cf31d91c1 /cfrontend | |
| parent | 0c36ecaed8fc861cb3e14b1396b0b6b6e754c199 (diff) | |
| download | compcert-c42707362b99da19cc7a3f2496d9620dcc0dfa62.tar.gz compcert-c42707362b99da19cc7a3f2496d9620dcc0dfa62.zip | |
Moved common buitlins to C2C gernic_builtins.
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index b194b84a..4dbd6c05 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -135,9 +135,19 @@ let string_of_errmsg msg = let builtins_generic = { Builtins.typedefs = []; Builtins.functions = [ + (* Integer arithmetic *) + "__builtin_bswap", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + "__builtin_bswap32", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + "__builtin_bswap16", + (TInt(IUShort, []), [TInt(IUShort, [])], false); (* Floating-point absolute value *) "__builtin_fabs", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* Float arithmetic *) + "__builtin_fsqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], |