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, 15 insertions, 0 deletions

diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 629a615..29197e9 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1082,6 +1082,21 @@ Proof.
   split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A.  
   destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
   auto.
+  (* Ccompfzero *)
+  generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. case c; apply MATCH; assumption.
+  auto.
+  (* Cnotcompf *)
+  generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A.  
+  destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
+  auto.
 Qed.
 
 (** Translation of arithmetic operations. *)