From 601569c2e0c9ec4748eefcbdb9f62c93f8aa822c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 4 Sep 2010 09:28:33 +0000
Subject: Support for __builtin_fmax and __builtin_fmin

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/CBuiltins.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'ia32/CBuiltins.ml')

diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index d077fe55..14a2f10c 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -24,5 +24,9 @@ let builtins = {
     (* Float arithmetic *)
     "__builtin_fsqrt",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+    "__builtin_fmax",
+      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+    "__builtin_fmin",
+      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
   ]
 }
-- 
cgit