|
definition:
|
printVerifyResults :: TermDomain a => Options -> String -> (QName -> Bool)
-> [FuncDecl] -> [(QName,ACallType a)]
-> [(QName,NonFailCond)] -> IO ()
printVerifyResults opts mname isvisible fdecls ctypes nfconds
| optVerb opts == 0
= return ()
| optFormat opts == FormatJSON
= putStrLn $ ppJSON $ JArray $
map callAType2JSON (sortFunResults (filter (showFun . fst) ctypes))
| optFormat opts == FormatXML
= putStrLn $ showXmlDoc $ xml "results" $
map callAType2XML (sortFunResults (filter (showFun . fst) ctypes))
| otherwise
= do
putStr $ "MODULE '" ++ mname ++ "' VERIFIED"
let calltypes = filter (\(qf,ct) -> not (isTotalACallType ct) && showFun qf)
ctypes
funconds = filter (showFun . fst) nfconds
if null calltypes
then putStrLn "\n"
else putStrLn $ unlines $ " W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:"
: showFunResults prettyFunCallAType
(sortFunResults (filter ((`notElem` (map fst funconds)) . fst)
calltypes))
unless (null funconds) $
putStrLn $ "NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:\n" ++
showConditions fdecls (sortFunResults funconds)
where
showFun qf = not (optPublic opts) || isvisible qf
callAType2JSON (qf@(mn,fn),fct) =
JObject [("module", JString mn),
("name" , JString fn),
("result", JString (showCallATypeOrNonFailCond qf fct))]
callAType2XML (qf@(mn,fn),fct) =
xml "operation" [xml "module" [xtxt mn],
xml "name" [xtxt fn],
xml "result" [xtxt (showCallATypeOrNonFailCond qf fct)]]
showCallATypeOrNonFailCond qf ct =
maybe ("0:" ++ show ct)
(\nfc -> "1:" ++ show (snd (genNonFailFunction fdecls (qf,nfc))))
(lookup qf nfconds)
|
|
signature:
|
Analysis.TermDomain.TermDomain a => Verify.Options.Options -> String
-> ((String, String) -> Prelude.Bool) -> [FlatCurry.Types.FuncDecl]
-> [((String, String), Prelude.Maybe [a])]
-> [((String, String), ([(Prelude.Int, FlatCurry.Types.TypeExpr)], FlatCurry.Types.Expr))]
-> Prelude.IO ()
|