diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2018-12-03 15:08:53 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-12-20 15:19:42 +0100 |
| commit | 50fd8fe358b0eacb92d4cc28b6ada062e38023f5 (patch) | |
| tree | 80aca4c074539d5c773e8eab476af133c9edbedf /common/Linking.v | |
| parent | 88e9a78529282605f097bff78c6604524d25b592 (diff) | |
| download | compcert-kvx-50fd8fe358b0eacb92d4cc28b6ada062e38023f5.tar.gz compcert-kvx-50fd8fe358b0eacb92d4cc28b6ada062e38023f5.zip | |
x86: wrong modeling of ZF flag for FP comparisons
As written in the comment, ZF should be set if the two floats are
equal or unordered. The "or unordered" case was missing in the
original modeling of FP comparisons.
- Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions.
- Update the proofs in Asmgenproof1 accordingly.
No change required to the code generated for FP comparisons: this code
already anticipated the "or unordered" case.
Problem reported by Alix Trieu.
Diffstat (limited to 'common/Linking.v')
0 files changed, 0 insertions, 0 deletions