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 /papers/cfrontend_new/syntax2.etex | |
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}.
Diffstat (limited to 'papers/cfrontend_new/syntax2.etex')
0 files changed, 0 insertions, 0 deletions