aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-07-25 17:47:25 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2020-07-27 16:30:28 +0200
commitbc20d7c0d16d07790fb6eb608bf608237b0abbc3 (patch)
treeecd53e2409e1762cd946a6ebb608b4c6aa30ef73 /x86
parenta56e0c65b08f0f7123630f3a1b415e67ef48c38e (diff)
downloadcompcert-kvx-bc20d7c0d16d07790fb6eb608bf608237b0abbc3.tar.gz
compcert-kvx-bc20d7c0d16d07790fb6eb608bf608237b0abbc3.zip
Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml
These functions are now available on all targets.
Diffstat (limited to 'x86')
-rw-r--r--x86/CBuiltins.ml13
1 files changed, 0 insertions, 13 deletions
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index e7f714c7..6820c089 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -30,19 +30,6 @@ let builtins = {
"__builtin_va_list", va_list_type;
];
builtin_functions = [
- (* Integer arithmetic *)
- "__builtin_clz",
- (TInt(IInt, []), [TInt(IUInt, [])], false);
- "__builtin_clzl",
- (TInt(IInt, []), [TInt(IULong, [])], false);
- "__builtin_clzll",
- (TInt(IInt, []), [TInt(IULongLong, [])], false);
- "__builtin_ctz",
- (TInt(IInt, []), [TInt(IUInt, [])], false);
- "__builtin_ctzl",
- (TInt(IInt, []), [TInt(IULong, [])], false);
- "__builtin_ctzll",
- (TInt(IInt, []), [TInt(IULongLong, [])], false);
(* Float arithmetic *)
"__builtin_fmax",
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);