|
definition:
|
verifyNonFailingMod :: Options -> String -> IO ()
verifyNonFailingMod opts modname = do
printWhenStatus opts $ "Analyzing module '" ++ modname ++ "':"
prog <- readSimpTypedFlatCurryWithSpec opts modname
let errs = checkContractUsage (progName prog)
(map (\fd -> (snd (funcName fd), funcType fd)) (progFuncs prog))
unless (null errs) $ do
putStr $ unlines (map showOpError errs)
exitWith 1
impprogs <- mapM (readSimpTypedFlatCurryWithSpec opts) (progImports prog)
let allprogs = prog : impprogs
vinfo = foldr addFunsToVerifyInfo (initVerifyInfo opts)
(map progFuncs allprogs)
vstate = foldr addProgToState (initVState vinfo) allprogs
siblingconsinfo <- loadAnalysisWithImports siblingCons prog
pi1 <- getProcessInfos
printWhenAll opts $ unlines $
["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line]
vstref <- newIORef vstate
proveNonFailingFuncs opts siblingconsinfo vstref (progFuncs prog)
stats <- readIORef vstref
pi2 <- getProcessInfos
let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
maybe 0 id (lookup ElapsedTime pi1)
when (optTime opts) $ putStrLn $
"TOTAL VERIFICATION TIME : " ++ show tdiff ++ " msec"
when (optVerb opts > 0 || not (isVerified stats)) $
putStr (showStats stats)
where
line = take 78 (repeat '-')
showOpError (qf,err) =
snd qf ++ " (module " ++ fst qf ++ "): " ++ err
|