diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-06 09:01:42 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-06 09:01:42 +0200 |
| commit | bec421ba348b0a511c7821843b04e5e9d7ccc619 (patch) | |
| tree | 068c62d4831690670cb715188d4a7b26295807f7 /powerpc/Asm.v | |
| parent | e2a117e9801a432ea2813b2a6cddf073733575d2 (diff) | |
| download | compcert-bec421ba348b0a511c7821843b04e5e9d7ccc619.tar.gz compcert-bec421ba348b0a511c7821843b04e5e9d7ccc619.zip | |
Tighten and prove correct the underflow/overflow bounds for parsing of FP literals.
This is a follow-up to commit 350354c.
- Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse
- Add early checks for overflow and underflow and prove them correct.
- Improve speed of Bparse by using a fast exponentiation (square-and-multiply).
Diffstat (limited to 'powerpc/Asm.v')
0 files changed, 0 insertions, 0 deletions