|
definition:
|
verifyModuleIfNew :: TermDomain a => Analysis a -> IORef ProgInfo
-> IORef (AnalysisStore a) -> Options -> String -> IO ()
verifyModuleIfNew valueanalysis pistore astore opts0 mname = do
z3exists <- fileInPath "z3"
let z3msg = "Option '--nosmt' activated since SMT solver Z3 not found in PATH!"
opts <- if z3exists || not (optSMT opts0)
then return opts0
else do printInfoLine z3msg
return opts0 { optSMT = False }
printWhenStatus opts $ "Processing module '" ++ mname ++ "':"
flatprog <- getFlatProgFor pistore mname
outdatedtypes <- typeFilesOutdated opts mname
if outdatedtypes || optRerun opts || not (null (optFunction opts))
then verifyModule valueanalysis pistore astore opts mname flatprog
else do
let fdecls = progFuncs flatprog
visfuncs = filter (\fn -> optGenerated opts || isCurryID fn)
(map funcName
(filter ((== Public) . funcVisibility)
fdecls))
visfuncset = Set.fromList visfuncs
isVisible qf = Set.member qf visfuncset
let qname = ("","") -- some (unused) QName
avalue = startValue valueanalysis -- some (unused) abstract type value
when (optIOTypes opts) $ do
printWhenStatus opts "Reading in/out types from previous verification..."
iotypes <- readIOTypes opts mname
-- note: the `asTypeOf` expression is necessary to convince the type
-- checker that `iotypes` is parametric over the type variable `a`:
printIOTypes opts
(filter (isVisible . fst)
(iotypes `asTypeOf` [(qname, valueInOutType avalue)]))
printWhenStatus opts "Reading call types from previous verification..."
(ctypes,nfconds) <- readCallCondTypes opts mname
-- note: the `asTypeOf` expression is necessary to convince the type
-- checker that `ctype` is parametric over the type variable `a`:
printVerifyResults opts mname isVisible fdecls
(ctypes `asTypeOf` [(qname, Just [avalue])]) nfconds
return ()
|