Exported names:
- Datatypes:
- VerifyInfo
- VState
- VStateM
- Constructors:
- VerifyInfo
- VState
- Fields:
- allFuncs
- currTAProgs
- failedFuncs
- nfConds
- numAllFuncs
- numFailTests
- numNFCFuncs
- numPatTests
- postConds
- preConds
- toolOpts
- trInfo
- uPostCond
- uPreCond
- vPostCond
- vPreCond
- Operations:
- addFailedFuncToStats
- addFunsToVerifyInfo
- addFunsToVerifyInfo'
- addPostCondToStats
- addPreCondToStats
- addProgsToState
- evalOption
- getOption
- incFailTestInStats
- incNumAllInStats
- incNumNFCInStats
- incPatTestInStats
- initVerifyInfo
- initVState
- isContractOp
- isProperty
- isVerifiedContracts
- isVerifiedFailfree
- modifyOptions
- printCP
- printWhenAll
- printWhenIntermediate
- printWhenStatus
- showContractStats
- showFailfreeStats
- showStats
- tdeclOf
- whenOption
Imported modules:

Module VerifierState

Summary of exported operations:

initVerifyInfo
                  ::  Options -> VerifyInfo

addFunsToVerifyInfo'
                  ::  [AFuncDecl TypeExpr] -> VerifyInfo -> VerifyInfo

isContractOp
                  ::  (String,String) -> Bool

Is an operation name the name of a contract or similar?

isProperty
                  ::  AFuncDecl TypeExpr -> Bool

Is a function declaration a property?

initVState
                  ::  Options -> VState

modifyOptions
                  ::  (Options -> Options) -> StateT VState IO ()

getOption
                  ::  (Options -> a) -> StateT VState IO a

evalOption
                  ::  (Options -> a) -> (a -> Bool) -> StateT VState IO () -> StateT VState IO ()

whenOption
                  ::  (Options -> Bool) -> StateT VState IO () -> StateT VState IO ()

printWhenStatus
                  ::  String -> StateT VState IO ()

printWhenIntermediate
                  ::  String -> StateT VState IO ()

printWhenAll
                  ::  String -> StateT VState IO ()

printCP
                  ::  String -> StateT VState IO ()

showFailfreeStats
                  ::  VState -> String

Shows the statistics for the failfree verification in human-readable format.

showContractStats
                  ::  VState -> String

Shows the statistics for the contract checking in human-readable format.

showStats
                  ::  StateT VState IO ()

Shows the statistics in human-readable format.

isVerifiedFailfree
                  ::  VState -> Bool

Are all non-failing properties verified?

isVerifiedContracts
                  ::  VState -> Bool

Are all contracts verified?

addFunsToVerifyInfo
                  ::  [AFuncDecl TypeExpr] -> StateT VState IO ()

addFailedFuncToStats
                  ::  String -> String -> StateT VState IO ()

Adds a possibly failing call in a functions and the called function.

incNumAllInStats
                  ::  StateT VState IO ()

Increments the number of all tested functions.

incNumNFCInStats
                  ::  StateT VState IO ()

Increments the number of operations with nonfail conditions.

incPatTestInStats
                  ::  StateT VState IO ()

Increments the number of missing pattern tests.

incFailTestInStats
                  ::  StateT VState IO ()

Increments the number of test of possible failure calls.

addPreCondToStats
                  ::  String -> Bool -> StateT VState IO ()

Increments the number of preconditions.

addPostCondToStats
                  ::  String -> Bool -> StateT VState IO ()

Adds an operation to the already processed operations with postconditions.

addProgsToState
                  ::  [AProg TypeExpr] -> StateT VState IO ()

Adds a new typed FlatCurry program to the state.

tdeclOf
                  ::  (String,String) -> StateT VState IO (Maybe TypeDecl)

Selects the type declaration of a type constructor from the state.

Exported datatypes:

VerifyInfo

Constructors:

VerifyInfo :: Options -> [TAFuncDecl] -> [TAFuncDecl] -> [TAFuncDecl] -> [TAFuncDecl] -> VerifyInfo
Fields:
- toolOpts :: Options
- allFuncs :: [TAFuncDecl]
- preConds :: [TAFuncDecl]
- postConds :: [TAFuncDecl]
- nfConds :: [TAFuncDecl]

VState

Constructors:

VState :: VerifyInfo -> [(String,String)] -> Int -> Int -> Int -> Int -> [String] -> [String] -> [String] -> [String] -> [TAProg] -> VState
Fields:
- trInfo :: VerifyInfo
- failedFuncs :: [(String,String)]
- numAllFuncs :: Int
- numNFCFuncs :: Int
- numPatTests :: Int
- numFailTests :: Int
- uPreCond :: [String]
- vPreCond :: [String]
- uPostCond :: [String]
- vPostCond :: [String]
- currTAProgs :: [TAProg]

VStateM

Type synonym: VStateM a = StateT VState IO a

Exported operations:

initVerifyInfo :: Options -> VerifyInfo

Further infos:

solution complete, i.e., able to compute all solutions

addFunsToVerifyInfo' :: [AFuncDecl TypeExpr] -> VerifyInfo -> VerifyInfo

isContractOp :: (String,String) -> Bool

Is an operation name the name of a contract or similar?

isProperty :: AFuncDecl TypeExpr -> Bool

Is a function declaration a property?

initVState :: Options -> VState

Further infos:

solution complete, i.e., able to compute all solutions

modifyOptions :: (Options -> Options) -> StateT VState IO ()

getOption :: (Options -> a) -> StateT VState IO a

evalOption :: (Options -> a) -> (a -> Bool) -> StateT VState IO () -> StateT VState IO ()

whenOption :: (Options -> Bool) -> StateT VState IO () -> StateT VState IO ()

printWhenStatus :: String -> StateT VState IO ()

printWhenIntermediate :: String -> StateT VState IO ()

printWhenAll :: String -> StateT VState IO ()

printCP :: String -> StateT VState IO ()

showFailfreeStats :: VState -> String

Shows the statistics for the failfree verification in human-readable format.

showContractStats :: VState -> String

Shows the statistics for the contract checking in human-readable format.

showStats :: StateT VState IO ()

Shows the statistics in human-readable format.

isVerifiedFailfree :: VState -> Bool

Are all non-failing properties verified?

Further infos:

solution complete, i.e., able to compute all solutions

isVerifiedContracts :: VState -> Bool

Are all contracts verified?

Further infos:

solution complete, i.e., able to compute all solutions

addFunsToVerifyInfo :: [AFuncDecl TypeExpr] -> StateT VState IO ()

addFailedFuncToStats :: String -> String -> StateT VState IO ()

Adds a possibly failing call in a functions and the called function.

incNumAllInStats :: StateT VState IO ()

Increments the number of all tested functions.

incNumNFCInStats :: StateT VState IO ()

Increments the number of operations with nonfail conditions.

incPatTestInStats :: StateT VState IO ()

Increments the number of missing pattern tests.

incFailTestInStats :: StateT VState IO ()

Increments the number of test of possible failure calls.

addPreCondToStats :: String -> Bool -> StateT VState IO ()

Increments the number of preconditions. If the first argument is true, a precondition has been verified.

addPostCondToStats :: String -> Bool -> StateT VState IO ()

Adds an operation to the already processed operations with postconditions. If the second argument is true, the postcondition of this operation has been verified.

addProgsToState :: [AProg TypeExpr] -> StateT VState IO ()

Adds a new typed FlatCurry program to the state.

tdeclOf :: (String,String) -> StateT VState IO (Maybe TypeDecl)

Selects the type declaration of a type constructor from the state.

Exported names:

Imported modules:

Summary of exported operations:

Exported datatypes:

Exported operations: