GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 11:22:33 +03:00
Code Issues Projects Releases Wiki Activity

Fix bugs in the signed right shift operation.

Browse Source 
Fixes #664.
This commit is contained in:
Brian Huffman 2019-11-26 22:23:00 -08:00
parent c859570234
commit 56f263895a
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Cryptol/Prims/Eval.hs
View File

@ -678,9 +678,8 @@ sshrV =
wlam $ \y ->
let signx = testBit x (fromInteger (i-1))
amt = fromInteger (bvVal y)
negv = (((-1) `shiftL` amt) .|. x) `shiftR` amt
posv = x `shiftR` amt
in return . VWord i . ready . WordVal . mkBv i $! if signx then negv else posv
x' = if signx then x - bit (fromInteger i) else x
in return . VWord i . ready . WordVal . mkBv i $! x' `shiftR` amt
-- | Signed carry bit.
scarryV :: Value