aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-07-27 09:54:00 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2020-07-27 17:06:34 +0200
commit77ce8ba291afa9f5629a160df440f9af6614f3ef (patch)
tree3888df3631e39df97cdb58a8f7e3914c40007e13 /common
parent70f105e623dddeb27be258fedb56bd0e9a59d190 (diff)
downloadcompcert-kvx-77ce8ba291afa9f5629a160df440f9af6614f3ef.tar.gz
compcert-kvx-77ce8ba291afa9f5629a160df440f9af6614f3ef.zip
Add __builtin_sqrt as synonymous for __builtin_fsqrt
__builtin_sqrt (no "f") is the name used by GCC and Clang.
Diffstat (limited to 'common')
-rw-r--r--common/Builtins0.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/common/Builtins0.v b/common/Builtins0.v
index 4afe6f1a..d84c9112 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -367,6 +367,7 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
:: ("__builtin_fabs", BI_fabs)
:: ("__builtin_fabsf", BI_fabsf)
:: ("__builtin_fsqrt", BI_fsqrt)
+ :: ("__builtin_sqrt", BI_fsqrt)
:: ("__builtin_negl", BI_negl)
:: ("__builtin_addl", BI_addl)
:: ("__builtin_subl", BI_subl)