diff options
| author | xavier.leroy <xavier.leroy@college-de-france.fr> | 2019-08-31 17:00:24 +0200 |
|---|---|---|
| committer | xavier.leroy <xavier.leroy@college-de-france.fr> | 2019-08-31 17:00:24 +0200 |
| commit | c243b565ab0744086e10efcfee16768f6c3cf880 (patch) | |
| tree | 48c3556e6538464b00d43f94ba7e12e2b416b714 | |
| parent | 25a39ae6be7a4b65e01d9bb6b1fd94688aa674b0 (diff) | |
| download | compcert-aarch64.tar.gz compcert-aarch64.zip | |
AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}aarch64
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}.
| -rw-r--r-- | aarch64/Op.v | 4 | ||||
| -rw-r--r-- | aarch64/PrintOp.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/Op.v b/aarch64/Op.v index 34c03c77..a7483d56 100644 --- a/aarch64/Op.v +++ b/aarch64/Op.v @@ -564,8 +564,8 @@ Definition type_of_condition (c: condition) : list typ := | Ccompluimm _ _ => Tlong :: nil | Ccomplshift _ _ _ => Tlong :: Tlong :: nil | Ccomplushift _ _ _ => Tlong :: Tlong :: nil - | Cmasklzero _ => Tint :: nil - | Cmasklnotzero _ => Tint :: nil + | Cmasklzero _ => Tlong :: nil + | Cmasklnotzero _ => Tlong :: nil | Ccompf _ => Tfloat :: Tfloat :: nil | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfzero _ => Tfloat :: nil 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]) -> |