ivory-quickcheck 0.2.0.3 → 0.2.0.4
raw patch · 3 files changed
+32/−28 lines, 3 filesdep ~base
Dependency ranges changed: base
Files
- ivory-quickcheck.cabal +3/−3
- src/Ivory/QuickCheck.hs +16/−15
- test/Test.hs +13/−10
ivory-quickcheck.cabal view
@@ -1,5 +1,5 @@ name: ivory-quickcheck-version: 0.2.0.3+version: 0.2.0.4 author: Galois, Inc. copyright: 2013 Galois, Inc. maintainer: leepike@galois.com@@ -14,11 +14,11 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory- tag: hackage-qc-0103+ tag: hackage-0.1.0.4 library exposed-modules: Ivory.QuickCheck- build-depends: base >= 4.6 && < 5,+ build-depends: base >= 4.7 && < 5, base-compat, monadLib, random,
src/Ivory/QuickCheck.hs view
@@ -1,15 +1,15 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE DataKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE ImplicitParams #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-name-shadowing #-} -- | Check properties of Ivory programs using random inputs. -- -- Example usage:--- +-- -- > [ivory| -- > struct foo -- > { foo_a :: Stored IFloat@@ -43,18 +43,19 @@ module Ivory.QuickCheck (check, checkWith, contract) where -import Prelude ()+import Prelude () import Prelude.Compat -import Control.Monad (replicateM,forM)-import Data.IORef (IORef,newIORef,readIORef,writeIORef)-import Data.List (transpose,find)+import Control.Monad (forM, replicateM)+import Data.IORef (IORef, newIORef, readIORef,+ writeIORef)+import Data.List (find, transpose) import Ivory.Compile.C.CmdlineFrontend import qualified Ivory.Eval as E import Ivory.Language import Ivory.Language.Proc import qualified Ivory.Language.Syntax as I-import System.IO.Unsafe (unsafeInterleaveIO)+import System.IO.Unsafe (unsafeInterleaveIO) import qualified Test.QuickCheck.Arbitrary as A import qualified Test.QuickCheck.Gen as G@@ -192,10 +193,10 @@ -> sampleArray m len ty I.TyStruct ty -> sampleStruct m ty- I.TyProc _ _ -> err - I.TyVoid -> err - I.TyPtr _ -> err - I.TyCArray _ -> err + I.TyProc _ _ -> err+ I.TyVoid -> err+ I.TyPtr _ -> err+ I.TyCArray _ -> err I.TyOpaque -> err where err = error $ "I don't know how to make values of type '" ++ show t ++ "'!"@@ -292,7 +293,7 @@ sampleArray m len ty = repeatIO $ do (vars, blcks) <- unzip <$> replicateM len (head <$> sampleType m ty) let init = [ I.InitExpr ty (I.ExpVar v) | v <- vars ]- (v, blck) <- mkLocal (I.TyArr len ty) (I.InitArray init)+ (v, blck) <- mkLocal (I.TyArr len ty) (I.InitArray init True) return (v, concat blcks ++ blck) repeatIO :: IO a -> IO [a]
test/Test.hs view
@@ -182,13 +182,15 @@ m10 :: Module m10 = package "foo10" (incl foo10)- + ----------------------- foo11 :: Def ('[Ix 10] ':-> ())-foo11 = L.proc "foo11" $ \n -> body $ do+foo11 = L.proc "foo11" $ \n ->+ requires (n >=? 0)+ $ body $ do x <- local (ival (0 :: Sint8))- for n $ \i -> do+ 0 `upTo` n $ \i -> do x' <- deref x store x $ x' + safeCast i @@ -198,7 +200,7 @@ ----------------------- foo12 :: Def ('[Uint8] ':-> Uint8)-foo12 = L.proc "foo12" $ \n -> +foo12 = L.proc "foo12" $ \n -> ensures (\r -> r ==? n) $ body $ do ifte_ (n ==? 0)@@ -212,7 +214,7 @@ ----------------------- foo13 :: Def ('[Uint8, Uint8] ':-> Uint8)-foo13 = L.proc "foo13" $ \x y -> +foo13 = L.proc "foo13" $ \x y -> requires (x <=? 15) $ requires (y <=? 15) $ body $ ret (x * y)@@ -233,10 +235,11 @@ ----------------------- foo15 :: Def ('[Ix 10] ':-> Uint8)-foo15 = L.proc "foo15" $ \n -> - ensures (\r -> r <=? 5) $- body $ do- n `times` \i -> do+foo15 = L.proc "foo15" $ \n ->+ requires (n >=? 0)+ $ ensures (\r -> r <=? 5)+ $ body $ do+ n `downTo` 0 $ \i -> do ifte_ (i >? 5) (ret 5) (ret $ safeCast i) ret 4 -- FIXME: Ivory.Opts.TypeCheck doesn't see above `ret`s @@ -258,7 +261,7 @@ ----------------------- foo18 :: Def ('[Ref s ('L.Struct "foo2")] ':-> Ref s ('L.Struct "foo2"))-foo18 = L.proc "foo18" $ \f -> +foo18 = L.proc "foo18" $ \f -> requires (checkStored (f ~> aFoo) (\a -> a >? 0)) $ requires (checkStored (f ~> aFoo) (\a -> a <? 10)) $ ensures (\r -> checkStored (r ~> aFoo) (\a -> a >? 1))