From 87de3969856cf6a5eb5e1615ec817a015ed90d1c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 21 Jan 2022 11:48:06 +0100 Subject: Return second arg for float min/max on x86. If both arguments are zero the second argument is returned independ from their sign. Bug 32640 --- x86/Builtins1.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'x86') diff --git a/x86/Builtins1.v b/x86/Builtins1.v index e5233ff5..7c77a488 100644 --- a/x86/Builtins1.v +++ b/x86/Builtins1.v @@ -42,14 +42,14 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | 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 + | Some Lt => f1 + | Some Eq | 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 + | Some Gt => f1 + | Some Eq | Some Lt | None => f2 end) end. -- cgit