From c243b565ab0744086e10efcfee16768f6c3cf880 Mon Sep 17 00:00:00 2001 From: "xavier.leroy" Date: Sat, 31 Aug 2019 17:00:24 +0200 Subject: AArch64: wrong expected type for arguments of Cmaskl{zero,notzero} The argument is of type Tlong, not Tint. This caused spurious errors in RTLtyping. Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l" to distinguish them from Cmask{zero,notzero}. --- aarch64/PrintOp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'aarch64/PrintOp.ml') diff --git a/aarch64/PrintOp.ml b/aarch64/PrintOp.ml index 1780104c..2d45e446 100644 --- a/aarch64/PrintOp.ml +++ b/aarch64/PrintOp.ml @@ -73,9 +73,9 @@ let print_condition reg pp = function | (Ccomplushift(c, s, a), [r1;r2]) -> fprintf pp "%a %slu %a %a" reg r1 (comparison_name c) reg r2 shift (s, a) | (Cmasklzero n, [r1]) -> - fprintf pp "%a & 0x%Lx == 0" reg r1 (camlint64_of_coqint n) + fprintf pp "%a &l 0x%Lx == 0" reg r1 (camlint64_of_coqint n) | (Cmasklnotzero n, [r1]) -> - fprintf pp "%a & 0x%Lx != 0" reg r1 (camlint64_of_coqint n) + fprintf pp "%a &l 0x%Lx != 0" reg r1 (camlint64_of_coqint n) | (Ccompf c, [r1;r2]) -> fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 | (Cnotcompf c, [r1;r2]) -> -- cgit