diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-10 15:43:03 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:26:44 +0200 |
commit | 822a6a12316aa043eea7f6aed4d730bc10a73d7b (patch) | |
tree | bfeee08920725b1e871cc5902c4d71e862318292 /arm/Op.v | |
parent | 7cd0af8ba5d737fa9c45bb9fa454b38e9704097a (diff) | |
download | compcert-822a6a12316aa043eea7f6aed4d730bc10a73d7b.tar.gz compcert-822a6a12316aa043eea7f6aed4d730bc10a73d7b.zip |
x86_64: branchless implementation of floatofintu and intuoffloat
The implementation uses float <-> signed 64-bit integer conversion
instructions, and is both efficient and branchless.
Based on a suggestion by RĂ©mi Hutin.
Diffstat (limited to 'arm/Op.v')
0 files changed, 0 insertions, 0 deletions