copilot 2.0.4 → 2.0.5
raw patch · 3 files changed
+67/−9 lines, 3 filesdep ~copilot-coredep ~copilot-language
Dependency ranges changed: copilot-core, copilot-language
Files
- Examples/Examples2.hs +17/−0
- Examples/Test.hs +47/−6
- copilot.cabal +3/−3
Examples/Examples2.hs view
@@ -1,3 +1,11 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Some more Copilot examples.++{-# LANGUAGE RebindableSyntax #-}+ module Examples2 ( examples2 ) where import Prelude ()@@ -25,6 +33,15 @@ fibSpec :: Spec fibSpec = do trigger "fib_out" true [arg fib]++counter :: Stream Bool -> Stream Bool + -> Stream Int32+counter inc reset = cnt+ where + cnt = if reset then 0+ else if inc then z + 1+ else z+ z = [0] ++ cnt -} nats :: Stream Word64
Examples/Test.hs view
@@ -13,7 +13,8 @@ import qualified Copilot.Compile.C99 as C99 import qualified Copilot.Compile.SBV as SBV import qualified Copilot.Tools.CBMC as M-import Control.Monad (when)+import Control.Monad (when, unless)+import Data.Maybe (catMaybes) import AddMult import Array@@ -24,11 +25,13 @@ import Examples import Examples2 import ExtFuns+import Languages import Local import LTLExamples import PTLTLExamples import Random import RegExpExamples+import Sat import StackExamples import StatExamples import VotingExamples@@ -38,6 +41,14 @@ main :: IO () main = do+ ls <- checkExists+ when (null ls) runTests+ unless (null ls) $ do putStrLn "*** Warning! ***"+ putStrLn "Cannot run tests in this directory. You have the following files or directories that would be deleted: "+ mapM_ putStrLn ls+ +runTests :: IO ()+runTests = do cleanup putStrLn "Testing addMult ..." addMult >> cleanup@@ -66,6 +77,9 @@ putStrLn "Testing extFuns ..." extFuns >> cleanup putStrLn ""+ putStrLn "Testing language ..."+ languages >> cleanup+ putStrLn "" putStrLn "Testing localEx ..." localEx >> cleanup putStrLn ""@@ -81,6 +95,9 @@ putStrLn "Testing regExpExamples ..." regExpExamples >> cleanup putStrLn ""+ putStrLn "Testing satExamples ..."+ satExamples >> cleanup+ putStrLn "" putStrLn "Testing stackExamples ..." stackExamples >> cleanup putStrLn ""@@ -97,6 +114,33 @@ -------------------------------------------------------------------------------- +cbmcName :: String+cbmcName = "cbmc_driver.c"++atomCBMC :: String+atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName++sbvCBMC :: String+sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName++--------------------------------------------------------------------------------++checkExists :: IO [String]+checkExists = do+ b0 <- nmBool doesDirectoryExist SBV.sbvDirName+ b1 <- nmBool doesDirectoryExist C99.c99DirName+ b2 <- nmBool doesFileExist cbmcName+ b3 <- nmBool doesDirectoryExist atomCBMC+ b4 <- nmBool doesDirectoryExist sbvCBMC+ return $ catMaybes $ map getName [b0, b1, b2, b3, b4]++ where+ getName (nm, bool) = if bool then Just nm else Nothing+ nmBool f nm = do b <- f nm + return (nm, b)++--------------------------------------------------------------------------------+ cleanup :: IO () cleanup = do @@ -106,15 +150,12 @@ b1 <- doesDirectoryExist C99.c99DirName when b1 (removeDirectoryRecursive C99.c99DirName) - let cbmc = "cbmc_driver.c"- b2 <- doesFileExist cbmc- when b2 (removeFile cbmc)+ b2 <- doesFileExist cbmcName+ when b2 (removeFile cbmcName) - let atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName b3 <- doesDirectoryExist atomCBMC when b3 (removeDirectoryRecursive atomCBMC) - let sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName b4 <- doesDirectoryExist sbvCBMC when b4 (removeDirectoryRecursive sbvCBMC)
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 2.0.4+version: 2.0.5 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -29,8 +29,8 @@ -fno-warn-orphans build-depends: base >= 4.0 && <5- , copilot-core- , copilot-language+ , copilot-core >= 0.2.3+ , copilot-language >= 0.3 , copilot-libraries , copilot-cbmc exposed-modules: Language.Copilot