copilot-cbmc 0.23 → 2.1.1

raw patch · 2 files changed

+23/−26 lines, 2 filesdep ~basedep ~bytestringdep ~copilot-c99setup-changedPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, bytestring, copilot-c99, copilot-core, copilot-sbv, pretty

API changes (from Hackage documentation)

Files

• Setup.hs +1/−16
• copilot-cbmc.cabal +22/−10

@@ -1,21 +1,6 @@ module Main ( main ) where -import System.Directory    (findExecutable) import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, postInst)-import System.Directory    (findExecutable)-import System.Exit         (exitWith, ExitCode(..))  main :: IO ()-main = defaultMainWithHooks simpleUserHooks{ postInst = checkDefSolver }- where checkDefSolver _ _ _ _ = do-                mbP <- findExecutable "cbmc"-                case mbP of-                   Nothing -> do putStrLn "***"-                                 putStrLn "*** The copilot-cbmc library requires the solver cbcm to be installed."-                                 putStrLn "*** The executable CBMC must be in your path."-                                 putStrLn "*** Please install CBMC and put it in your path!"-                                 putStrLn "*** CBMC can downloaded at http://www.cprover.org/cbmc/"-                                 putStrLn "***"-                   Just _  -> return ()-                exitWith ExitSuccess-+main = defaultMain 

@@ -1,14 +1,26 @@ cabal-version             : >= 1.10 name                      : copilot-cbmc-version                   : 0.23+version                   : 2.1.1 synopsis                  : Copilot interface to a C model-checker.-description               : Depends on CBMC <http://www.cprover.org/cbmc/>.  Generates a driver to prove the Atom and SBV backends generate equivalent code.+description               :+  Depends on CBMC <http://www.cprover.org/cbmc/>.  Generates a driver to prove+  the Atom and SBV backends generate equivalent code.+  .+  Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in+  Haskell that compiles into embedded C.  Copilot contains an interpreter,+  multiple back-end compilers, and other verification tools.  A tutorial, bug+  reports, and todos are available at+  <https://github.com/leepike/copilot-discussion>.+  .+  Examples are available at+  <https://github.com/leepike/Copilot/tree/master/Examples>.+ license                   : BSD3 license-file              : LICENSE maintainer                : leepike@galois.com stability                 : Experimental category                  : Language, Embedded-build-type                : Custom+build-type                : Simple extra-source-files        : README.md  author                    : Lee Pike@@ -17,7 +29,7 @@  source-repository head     type:       git-    location:   git://github.com/niswegmann/copilot-cbmc.git+    location:   git://github.com/leepike/copilot-cbmc.git  library   default-language        : Haskell2010@@ -25,13 +37,13 @@   ghc-options             : -Wall -fwarn-tabs   ghc-prof-options        : -auto-all -caf-all -  build-depends           : base >= 4.3 && < 5-                          , bytestring-                          , copilot-core+  build-depends           : base >= 4.0 && <= 5.0+                          , bytestring >= 0.9+                          , copilot-core >= 0.2.4                           , directory >= 1.1                           , process >= 1.0-                          , pretty-                          , copilot-sbv-                          , copilot-c99+                          , pretty >= 1.0.1+                          , copilot-sbv >= 0.6+                          , copilot-c99 >= 0.2.4    exposed-modules         : Copilot.Tools.CBMC