|
definition:
|
verifyMod :: String -> VStateM ()
verifyMod modname = do
printWhenStatus $ "Analyzing module '" ++ modname ++ "':"
oprog <- readTypedFlatCurryWithSpec modname
let errs = checkContractUsage (progName oprog)
(map (\fd -> (snd (funcName fd), funcType fd)) (progFuncs oprog))
unless (null errs) $ lift $ do
putStr $ unlines (map showOpError errs)
exitWith 1
let prog = simpProg oprog
failfree <- getOption optFailfree
impprogs <- if failfree
then mapM readSimpTypedFlatCurryWithSpec $ progImports prog
else return []
let allprogs = prog : impprogs
addProgsToState allprogs
addFunsToVerifyInfo $ concatMap progFuncs allprogs
whenOption optInferNFCs $ do
siblingconsinfo <- lift $ loadAnalysisWithImports siblingConsAndDecl prog
inferNFCs modname siblingconsinfo
pi1 <- lift getProcessInfos
progWithNFCs <- lookupProg modname
printWhenAll $ unlines $
["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg oprog), line,
"TRANSFORMED PROGRAM:", line, showCurryModule (unAnnProg progWithNFCs), line]
whenOption optFailfree $ proveNonFailingFuncs prog
evalOption optContract (> 0) $ do
modifyOptions (\opts -> opts { optConFail = True })
prog1 <- verifyPostConditions oprog >>= verifyPreConditions
whenOption (\o -> optFCY o || optAFCY o) $ do
prog2 <- addPreConditions prog1
tprog <- lift $ do
ccprog <- fromJust <$>
readTypedFlatCurryFromPath "include" "ContractChecks"
let ccfuncs = progFuncs (rnmProg modname ccprog)
return $ updProgFuncs (++ ccfuncs) prog2
printWhenAll $ unlines $
["TRANSFORMED PROGRAM WITH CONTRACT CHECKING:", line,
showCurryModule (unAnnProg tprog), line]
whenOption optFCY $ lift $ writeFlatCurry $ unAnnProg tprog
whenOption optAFCY $ lift $ writeTypeAnnotatedFlatCurry tprog
pi2 <- lift $ getProcessInfos
let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
maybe 0 id (lookup ElapsedTime pi1)
whenOption optTime $ lift $ putStrLn $
"TOTAL VERIFICATION TIME : " ++ show tdiff ++ " msec"
showStats
where
line = take 78 (repeat '-')
showOpError (qf,err) =
snd qf ++ " (module " ++ fst qf ++ "): " ++ err
|