aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintOp.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-03-29 11:57:33 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-03-29 11:57:33 +0000
commit448cc3ff32cc60f4b9e78911404106797e109d90 (patch)
tree4dcea174d56a4984238d014c481c8d484d653007 /arm/PrintOp.ml
parentbf138748416195df13f68c097c750e1d388ac0de (diff)
downloadcompcert-kvx-448cc3ff32cc60f4b9e78911404106797e109d90.tar.gz
compcert-kvx-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/PrintOp.ml')
-rw-r--r--arm/PrintOp.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index 9ebce979..8f21cd41 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -48,6 +48,10 @@ let print_condition reg pp = function
fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2
| (Cnotcompf c, [r1;r2]) ->
fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2
+ | (Ccompfzero c, [r1]) ->
+ fprintf pp "%a %sf 0.0" reg r1 (comparison_name c)
+ | (Cnotcompfzero c, [r1]) ->
+ fprintf pp "%a not(%sf) 0.0" reg r1 (comparison_name c)
| _ ->
fprintf pp "<bad condition>"