Added semantic for AArch64 built-in function fmin/fmax.

The semantic is defined similar to the one from x86.
Bug 30035

Author: bschommer

aarch64/Builtins1.v

@@ -19,15 +19,35 @@ Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+  | BI_fmin
+  | BI_fmax.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+    ("__builtin_fmin", BI_fmin)
+  :: ("__builtin_fmax", BI_fmax)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_fmin | BI_fmax =>
+      mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_fmin =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Lt => f1
+                      | Some Gt | None => f2
+                      end)
+  | BI_fmax =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Gt => f1
+                      | Some Lt | None => f2
+                      end)
+  end.