GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-09 17:15:06 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1053 from GaloisInc/issue1049

Browse Source 
Fix the binary encoding of floating-point values.
This commit is contained in:
robdockins 2021-01-28 10:43:47 -08:00 committed by GitHub
commit 7eba2307b4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/Backend/FloatHelpers.hs
View File

@ -234,7 +234,7 @@ floatToBits e p bf = (isNeg `shiftL` (e' + p'))
case num of
Zero -> (0,0)
Num i ev
| ex == 0 -> (0, i `shiftL` (p' - m -1))
| ex <= 0 -> (0, i `shiftL` (p' - m -1 + fromInteger ex))
| otherwise -> (ex, (i `shiftL` (p' - m)) .&. pMask)
where
m = msb 0 i - 1

2
tests/issues/issue1049.icry Normal file
View File

@ -0,0 +1,2 @@
:m Float
:exhaust (\x -> (y != y \/ x == fpToBits y where y = fpFromBits x : Float16))

6
tests/issues/issue1049.icry.stdout Normal file
View File

@ -0,0 +1,6 @@
Loading module Cryptol
Loading module Cryptol
Loading module Float
Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.