copilot-cbmc 2.1.1 → 2.1.2
raw patch · 2 files changed
+16/−15 lines, 2 filesdep ~basePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base
API changes (from Hackage documentation)
Files
- copilot-cbmc.cabal +2/−2
- src/Copilot/Tools/CBMC.hs +14/−13
copilot-cbmc.cabal view
@@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-cbmc-version : 2.1.1+version : 2.1.2 synopsis : Copilot interface to a C model-checker. description : Depends on CBMC <http://www.cprover.org/cbmc/>. Generates a driver to prove@@ -37,7 +37,7 @@ ghc-options : -Wall -fwarn-tabs ghc-prof-options : -auto-all -caf-all - build-depends : base >= 4.0 && <= 5.0+ build-depends : base >= 4.0 && < 5.0 , bytestring >= 0.9 , copilot-core >= 0.2.4 , directory >= 1.1
src/Copilot/Tools/CBMC.hs view
@@ -3,6 +3,7 @@ -------------------------------------------------------------------------------- {-# LANGUAGE GADTs #-}+{-# LANGUAGE Rank2Types #-} module Copilot.Tools.CBMC ( Params (..)@@ -148,18 +149,18 @@ -------------------------------------------------------------------------------- typeSpec :: UType -> Doc-typeSpec UType { uTypeType = t } = text (typeSpec' t)- where- typeSpec' Bool = "bool"- typeSpec' Int8 = "int8_t"- typeSpec' Int16 = "int16_t"- typeSpec' Int32 = "int32_t"- typeSpec' Int64 = "int64_t"- typeSpec' Word8 = "uint8_t"- typeSpec' Word16 = "uint16_t"- typeSpec' Word32 = "uint32_t"- typeSpec' Word64 = "uint64_t"- typeSpec' Float = "float"- typeSpec' Double = "double"+typeSpec UType { uTypeType = t } = text $+ case t of+ Bool -> "bool"+ Int8 -> "int8_t"+ Int16 -> "int16_t"+ Int32 -> "int32_t"+ Int64 -> "int64_t"+ Word8 -> "uint8_t"+ Word16 -> "uint16_t"+ Word32 -> "uint32_t"+ Word64 -> "uint64_t"+ Float -> "float"+ Double -> "double" --------------------------------------------------------------------------------