|
definition:
|
initVerifyState :: TermDomain a => IORef ProgInfo -> Prog -> [(QName,ConsInfo)]
-> Map.Map QName (ACallType a) -> Map.Map QName NonFailCond
-> Map.Map QName (ACallType a)
-> Map.Map QName (InOutType a)
-> [(QName,NonFailCond)] -> Options
-> IO (VerifyState a)
initVerifyState pistore flatprog consinfos impacalltypes impfconds acalltypes
iotypes nfconds opts = do
unless (null nonfailconds) $ printWhenDetails opts $
"INITIAL NON-FAIL CONDITIONS:\n" ++
showConditions (progFuncs flatprog) nonfailconds
return $ VerifyState pistore (progName flatprog) (("",""),0,[]) consinfos 0
[] [] id impacalltypes nfacalltypes iotypes [] [] []
impfconds nonfailconds [] (0,0,0) opts False
where
nonfailconds = unionBy (\x y -> fst x == fst y) nfconds
(nonFailCondsOfModule flatprog)
-- set the call types of operations with non-fail conditions to "failed"
nfacalltypes = Map.insertList
(map (\(qf,_) -> (qf, failACallType)) nonfailconds)
acalltypes
|
|
signature:
|
Analysis.TermDomain.TermDomain a => Data.IORef.IORef Verify.ProgInfo.ProgInfo
-> FlatCurry.Types.Prog
-> [((String, String), (Prelude.Int, Verify.ProgInfo.ConsType, [((String, String), Prelude.Int)]))]
-> Data.Map.Map (String, String) (Prelude.Maybe [a])
-> Data.Map.Map (String, String) ([(Prelude.Int, FlatCurry.Types.TypeExpr)], FlatCurry.Types.Expr)
-> Data.Map.Map (String, String) (Prelude.Maybe [a])
-> Data.Map.Map (String, String) (Verify.IOTypes.InOutType a)
-> [((String, String), ([(Prelude.Int, FlatCurry.Types.TypeExpr)], FlatCurry.Types.Expr))]
-> Verify.Options.Options -> Prelude.IO (VerifyState a)
|