copilot 2.2.0 → 2.2.1
raw patch · 5 files changed
+44/−19 lines, 5 filesdep ~copilot-c99dep ~copilot-cbmcdep ~copilot-corenew-uploaderPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-c99, copilot-cbmc, copilot-core, copilot-language, copilot-libraries, copilot-sbv, copilot-theorem
API changes (from Hackage documentation)
Files
- Examples/Examples.hs +11/−1
- Examples/Examples2.hs +2/−1
- Examples/ExtFuns.hs +2/−2
- Examples/Test.hs +14/−0
- copilot.cabal +15/−15
Examples/Examples.hs view
@@ -99,11 +99,18 @@ ex2 = extern "e2" (Just e2) in ex1 + ex2 +latch :: Stream Bool -> Stream Bool+latch x = y+ where + y = if x then not z else z+ z = [False] ++ y+ --- Some infinite lists for simulating external variables: e1, e2 :: [Word64] e1 = [0..] e2 = 5 : 4 : e2-+a :: Stream Bool+a = [False, False, True, True ] ++ a -------------------------------------------------------------------------------- --@@ -155,4 +162,7 @@ reify spec >>= C.genCBMC C.defaultParams {C.numIterations = 20} +test :: Spec+test = do+ observer "obs" (latch a) --------------------------------------------------------------------------------
Examples/Examples2.hs view
@@ -71,4 +71,5 @@ examples2 :: IO () examples2 = do -- reify fibSpec >>= S.compile S.defaultParams- reify spec >>= S.compile S.defaultParams +-- reify spec >>= S.compile S.defaultParams + reify spec >>= S.compile (S.Params { S.prefix = Just "secondexamplespec" })
Examples/ExtFuns.hs view
@@ -53,8 +53,8 @@ extFuns :: IO () extFuns = do interpret 10 spec- reify spec >>= C.compile C.defaultParams - reify spec >>= S.compile S.defaultParams +--- reify spec >>= C.compile C.defaultParams + reify spec >>= S.compile (S.Params { S.prefix = Just "externFunSpec" }) --------------------------------------------------------------------------------
Examples/Test.hs view
@@ -117,6 +117,13 @@ cbmcName :: String cbmcName = "cbmc_driver.c" +exam2Name :: String+exam2Name = "secondexamplespec_copilot-sbv-codegen"++examsbvName :: String+examsbvName = "externFunSpec_copilot-sbv-codegen"++ atomCBMC :: String atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName @@ -158,5 +165,12 @@ b4 <- doesDirectoryExist sbvCBMC when b4 (removeDirectoryRecursive sbvCBMC)++ b5 <- doesDirectoryExist exam2Name+ when b5 (removeDirectoryRecursive exam2Name)+ ++ b6 <- doesDirectoryExist examsbvName+ when b6 (removeDirectoryRecursive examsbvName) --------------------------------------------------------------------------------
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 2.2.0+version: 2.2.1 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -38,13 +38,13 @@ -fno-warn-orphans build-depends: base >= 4.0 && < 5- , copilot-core == 2.2.0- , copilot-theorem == 0.2- , copilot-language == 2.2.0- , copilot-libraries == 2.2.0- , copilot-sbv == 2.2.0- , copilot-cbmc == 2.1.2- , copilot-c99 == 2.2.0+ , copilot-core >= 2.2.1+ , copilot-theorem >= 2.2.1+ , copilot-language >= 2.2.1+ , copilot-libraries >= 2.2.1+ , copilot-sbv >= 2.2.1+ , copilot-cbmc >= 2.2.1+ , copilot-c99 >= 2.2.1 exposed-modules: Language.Copilot @@ -55,13 +55,13 @@ main-is : Test.hs build-depends: base >= 4.0 && < 5- , copilot-core == 2.2.0- , copilot-theorem == 0.2- , copilot-language == 2.2.0- , copilot-libraries == 2.2.0- , copilot-sbv == 2.2.0- , copilot-cbmc == 2.1.2- , copilot-c99 == 2.2.0+ , copilot-core >= 2.2.1+ , copilot-theorem >= 2.2.1+ , copilot-language >= 2.2.1+ , copilot-libraries >= 2.2.1+ , copilot-sbv >= 2.2.1+ , copilot-cbmc >= 2.2.1+ , copilot-c99 >= 2.2.1 , directory >= 1.2.1 , random other-modules: AddMult