aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
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)