sbv 8.11 → 8.12

raw patch · 5 files changed

+11/−6 lines, 5 files

Files

• CHANGES.md +6/−1
• Data/SBV/List.hs +1/−1
• Data/SBV/Utils/CrackNum.hs +2/−2
• Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs +1/−1
• sbv.cabal +1/−1

@@ -1,7 +1,12 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 8.11, 2021-03-09+* Latest Hackage released version: 8.12, 2021-03-09++### Version 8.12, 2021-03-09++  * Fix a bug in crackNum for unsigned-integer values, which incorrectly+    showed a negation sign for values with msb set to 1.  ### Version 8.11, 2021-03-09 

@@ -99,7 +99,7 @@  | True  = subList l 1 (length l - 1) --- | @`uncons` returns the pair of the head and tail. Unspecified if the list is empty.+-- | @`uncons`@ returns the pair of the head and tail. Unspecified if the list is empty. uncons :: SymVal a => SList a -> (SBV a, SList a) uncons l = (head l, tail l) 

@@ -95,8 +95,8 @@           | True   = "Unsigned " ++ show sz ++ "-bit word"          signBit = v `testBit` (sz-1)-        s | signBit = "-"-          | True    = ""+        s | signed && signBit = "-"+          | True              = ""          av = abs v 

@@ -21,7 +21,7 @@ -- Note how we use the overflow checking variants of the arithmetic operators. We have: -- -- >>> checkArithOverflow midPointBroken--- Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:35:28:+!: SInt32 addition overflows: Violated. Model:+-- Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:35:32:+!: SInt32 addition overflows: Violated. Model: --   low  = 2147483647 :: Int32 --   high = 2147483647 :: Int32 --

@@ -1,7 +1,7 @@ Cabal-Version: 2.2  Name        : sbv-Version     : 8.11+Version     : 8.12 Category    : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis    : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT