Module Verify.Options

The options of the verification tool together with some related operations.

Author: Michael Hanus

Version: October 2024

Summary of exported operations:

defaultOptions :: Options  Deterministic 
The default options of the verification tool.
processOptions :: String -> [String] -> IO (Options,[String])  Deterministic 
Process the actual command line argument and return the options and the name of the main program.
whenStatus :: Options -> IO () -> IO ()  Deterministic 
printWhenStatus :: Options -> String -> IO ()  Deterministic 
printWhenDetails :: Options -> String -> IO ()  Deterministic 
printWhenAll :: Options -> String -> IO ()  Deterministic 

Exported datatypes:

OutputFormat

The type of supported output formats of verification results.

Constructors:

  • FormatText :: OutputFormat
  • FormatJSON :: OutputFormat
  • FormatXML :: OutputFormat
Options

Constructors:

  • Options :: Int -> Bool -> String -> Bool -> Bool -> Bool -> OutputFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> String -> Options

    Fields:

    • optVerb :: Int
    • optHelp :: Bool
    • optFunction :: String
    • optImports :: Bool
    • optDeleteCache :: Bool
    • optEnforceNF :: Bool
    • optFormat :: OutputFormat
    • optRerun :: Bool
    • optPublic :: Bool
    • optGenerated :: Bool
    • optCallTypes :: Bool
    • optIOTypes :: Bool
    • optVerify :: Bool
    • optSMT :: Bool
    • optStoreFuncs :: Bool
    • optStoreSMT :: Bool
    • optError :: Bool
    • optSpecModule :: Bool
    • optStats :: Bool
    • optTime :: Bool
    • optDomainID :: String

Exported operations:

defaultOptions :: Options  Deterministic 

The default options of the verification tool.

Further infos:
  • solution complete, i.e., able to compute all solutions

processOptions :: String -> [String] -> IO (Options,[String])  Deterministic 

Process the actual command line argument and return the options and the name of the main program.

whenStatus :: Options -> IO () -> IO ()  Deterministic 

printWhenStatus :: Options -> String -> IO ()  Deterministic 

printWhenDetails :: Options -> String -> IO ()  Deterministic 

printWhenAll :: Options -> String -> IO ()  Deterministic