diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-12 11:42:25 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:16:00 +0200 |
commit | 8b0de52ffa302298abe8d0d6e3b6ed339a2354ba (patch) | |
tree | fcfdb40451908865ba706e184ff434a847b7711b /backend/SplitLong.vp | |
parent | dc5dc1da4cfa10647d13f393b6685f962b9b9faa (diff) | |
download | compcert-8b0de52ffa302298abe8d0d6e3b6ed339a2354ba.tar.gz compcert-8b0de52ffa302298abe8d0d6e3b6ed339a2354ba.zip |
Add floating-point square root and fused multiply-add
We just lift the corresponding functions from Flocq and add
the computation of NaN payloads.
NaN payloads for FMA are described in the ARM and RISC-V specifications,
and were determined experimentally for x86 and for Power.
Diffstat (limited to 'backend/SplitLong.vp')
0 files changed, 0 insertions, 0 deletions