GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity

Support toInteger/fromInteger with symbolic arguments in :prove/:sat.

Browse Source
This commit is contained in:
Brian Huffman 2017-09-14 17:51:03 -07:00
parent 5332d98261
commit 571d186c6c
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Cryptol/Symbolic/Value.hs
View File

@ -211,14 +211,14 @@ instance BitWord SBool SWord SInteger where
svToInteger :: SWord -> SInteger
svToInteger w =
case svAsInteger w of
Nothing -> evalPanic "toInteger" ["unsupported symbolic argument"]
Nothing -> svFromIntegral KUnbounded w
Just x -> svInteger KUnbounded x
-- TODO: implement this properly in SBV using "int2bv"
svFromInteger :: Integer -> SInteger -> SWord
svFromInteger n i =
case svAsInteger i of
Nothing -> evalPanic "fromInteger" ["unsupported symbolic argument"]
Nothing -> svFromIntegral (KBounded False (fromInteger n)) i
Just x -> literalSWord (fromInteger n) x
-- Errors ----------------------------------------------------------------------