diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-29 11:57:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-29 11:57:33 +0000 |
commit | 448cc3ff32cc60f4b9e78911404106797e109d90 (patch) | |
tree | 4dcea174d56a4984238d014c481c8d484d653007 /arm/Asmgen.v | |
parent | bf138748416195df13f68c097c750e1d388ac0de (diff) | |
download | compcert-448cc3ff32cc60f4b9e78911404106797e109d90.tar.gz compcert-448cc3ff32cc60f4b9e78911404106797e109d90.zip |
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
Diffstat (limited to 'arm/Asmgen.v')
-rw-r--r-- | arm/Asmgen.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index c727db9b..7cf25f5f 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)]. |