|
definition: |
main :: IO ()
main = do
args <- getArgs
(opts0,progs) <- processOptions banner args
-- set analysis to top values if unspecified
let opts = if null (optDomainID opts0)
then opts0 { optDomainID = analysisName resultValueAnalysisTop }
else opts0
when (optDeleteCache opts0) $ deleteVerifyCacheDirectory opts0
case progs of
[] -> unless (optDeleteCache opts0) $ do
printInfoLine "Module name missing!"
printInfoLine "Try option '--help' for usage information."
exitWith 1
ms -> do
if optDomainID opts == analysisName resultValueAnalysisTop
then runWith resultValueAnalysisTop opts ms
else
if optDomainID opts == analysisName resultValueAnalysis2
then runWith resultValueAnalysis2 opts ms
else
if optDomainID opts == analysisName resultValueAnalysis5
then runWith resultValueAnalysis5 opts ms
else error "Unknown analysis domain ID!"
where
runWith analysis opts ms = do
printWhenStatus opts banner
pistore <- newIORef emptyProgInfo
astore <- newIORef (AnaStore [])
mapM_ (runModuleAction (verifyModuleIfNew analysis pistore astore opts)) ms
|
|
demand: |
no demanded arguments |
|
deterministic: |
deterministic operation |
|
indeterministic: |
might be indeterministic |
|
infix: |
no fixity defined |
|
name: |
main |
|
precedence: |
no precedence defined |
|
result-values: |
_ |
|
signature: |
Prelude.IO () |
|
solution-complete: |
operation might suspend on free variables |
|
terminating: |
possibly non-terminating |
|
totally-defined: |
possibly non-reducible on same data term |