mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-17 09:50:35 +03:00
Fix off-by-one error in What4 implementation of (@)
In the case where the index is a symbolic `Integer` and the sequence is of length `n`, the What4 backend mistakenly chose `n` to be the largest possible index. This corrects it to instead be `n - 1`. Fixes #1359.
This commit is contained in:
parent
9e59289457
commit
c37a71b4c5
@ -1,3 +1,10 @@
|
||||
# next
|
||||
|
||||
## Bug fixes
|
||||
|
||||
* Fix a bug in the What4 backend that could cause applications of `(@)` with
|
||||
symbolic `Integer` indices to become out of bounds (#1359).
|
||||
|
||||
# 2.13.0
|
||||
|
||||
## Language changes
|
||||
|
@ -540,7 +540,7 @@ indexFront_int sym mblen _a xs _ix idx
|
||||
-- isn't much we can do.
|
||||
maxIdx =
|
||||
case mblen of
|
||||
Nat n -> Just n
|
||||
Nat n -> Just (n - 1)
|
||||
Inf -> Nothing
|
||||
indexFront_segs ::
|
||||
W4.IsSymExprBuilder sym =>
|
||||
|
7
tests/issues/issue1359.icry
Normal file
7
tests/issues/issue1359.icry
Normal file
@ -0,0 +1,7 @@
|
||||
:set prover=sbv-z3
|
||||
:safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)
|
||||
:safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))
|
||||
|
||||
:set prover=w4-z3
|
||||
:safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)
|
||||
:safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))
|
5
tests/issues/issue1359.icry.stdout
Normal file
5
tests/issues/issue1359.icry.stdout
Normal file
@ -0,0 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Safe
|
||||
Safe
|
||||
Safe
|
||||
Safe
|
Loading…
Reference in New Issue
Block a user