From 448cc3ff32cc60f4b9e78911404106797e109d90 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 29 Mar 2012 11:57:33 +0000
Subject: Support for fcmpzd instruction (float compare with +0.0)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1858 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/PrintAsm.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'arm/PrintAsm.ml')

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 634faae1..48943e98 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -562,16 +562,16 @@ let print_instruction oc = function
   | Pfsubd(r1, r2, r3) ->
       fprintf oc "	fsubd	%a, %a, %a\n" freg r1 freg r2 freg r3; 1
   | Pflid(r1, f) ->
-(*
-      if Int64.bits_of_float f = 0L (* +0.0 *) then begin
-        fprintf oc "	mvfd	%a, #0.0\n" freg r1; 1
-      end else begin
-*)
+      (* We could make good use of the fconstd instruction, but it's available
+         in VFD v3 and up, not in v1 nor v2 *)
       let lbl = label_float f in
       fprintf oc "	fldd	%a, .L%d @ %.12g\n" freg r1 lbl f; 1
   | Pfcmpd(r1, r2) ->
       fprintf oc "	fcmpd	%a, %a\n" freg r1 freg r2;
       fprintf oc "	fmstat\n"; 2
+  | Pfcmpzd(r1) ->
+      fprintf oc "	fcmpzd	%a\n" freg r1;
+      fprintf oc "	fmstat\n"; 2
   | Pfsitod(r1, r2) ->
       fprintf oc "	fmsr	%a, %a\n" freg_single r1 ireg r2;
       fprintf oc "	fsitod	%a, %a\n" freg r1 freg_single r1; 2
-- 
cgit