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

Use correct default value for symbolic indexing. Fixes #388.

Browse Source 
We now use the zero value of the element type as the
default; previously we were incorrectly using the zero
value of the *index* type.
This commit is contained in:
Brian Huffman 2016-12-13 17:40:57 -08:00
parent e48f430b30
commit 08a7982a46
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/Symbolic/Prims.hs
View File

@ -333,7 +333,7 @@ indexFront mblen a xs idx
where
k = SBV.kindOf idx
w = SBV.intSizeOf idx
def = ready $ VWord (toInteger w) $ ready $ WordVal $ SBV.svInteger k 0
def = ready $ zeroV a
f n y = iteValue (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y