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

1 files changed, 6 insertions, 0 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index c727db9..7cf25f5 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -155,6 +155,10 @@ Definition transl_cond
       Pfcmpd (freg_of a1) (freg_of a2) :: k
   | Cnotcompf cmp, a1 :: a2 :: nil =>
       Pfcmpd (freg_of a1) (freg_of a2) :: k
+  | Ccompfzero cmp, a1 :: nil =>
+      Pfcmpzd (freg_of a1) :: k
+  | Cnotcompfzero cmp, a1 :: nil =>
+      Pfcmpzd (freg_of a1) :: k
   | _, _ =>
      k (**r never happens for well-typed code *)
   end.
@@ -209,6 +213,8 @@ Definition crbit_for_cond (cond: condition) :=
   | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp
   | Ccompf cmp => crbit_for_float_cmp cmp
   | Cnotcompf cmp => crbit_for_float_not_cmp cmp
+  | Ccompfzero cmp => crbit_for_float_cmp cmp
+  | Cnotcompfzero cmp => crbit_for_float_not_cmp cmp
   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].