aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
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 /cfrontend
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 'cfrontend')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index c7cd4937..2386eed9 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -200,6 +200,8 @@ let builtins_generic = {
(* Float arithmetic *)
"__builtin_fsqrt",
(TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+ "__builtin_sqrt",
+ (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
(* Block copy *)
"__builtin_memcpy_aligned",
(TVoid [],