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 /debug | |
| parent | dc5dc1da4cfa10647d13f393b6685f962b9b9faa (diff) | |
| download | compcert-kvx-8b0de52ffa302298abe8d0d6e3b6ed339a2354ba.tar.gz compcert-kvx-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 'debug')
0 files changed, 0 insertions, 0 deletions