Exported names:
- Datatypes:
- VerifyInfo
- VState
- Constructors:
- VerifyInfo
- VState
- Fields:
- allFuncs
- currTAProgs
- failedFuncs
- nfConds
- numAllFuncs
- numFailTests
- numNFCFuncs
- numPatTests
- postConds
- preConds
- toolOpts
- trInfo
- Operations:
- addFailedFuncToStats
- addFunsToVerifyInfo
- addProgToState
- incFailTestInStats
- incNumAllInStats
- incNumNFCInStats
- incPatTestInStats
- initVerifyInfo
- initVState
- isContractOp
- isProperty
- isVerified
- readVerifyInfoRef
- showStats
- tdeclOf
Imported modules:

Module VerifierState

Summary of exported operations:

initVerifyInfo
                  ::  Options -> VerifyInfo

Deterministic

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

Deterministic

isContractOp
                  ::  (String,String) -> Bool

Deterministic

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

isProperty
                  ::  AFuncDecl TypeExpr -> Bool

Deterministic

Is a function declaration a property?

initVState
                  ::  VerifyInfo -> VState

Deterministic

readVerifyInfoRef
                  ::  IORef VState -> IO VerifyInfo

Deterministic

Reads VerifyInfo from VState IORef.

showStats
                  ::  VState -> String

Deterministic

Shows the statistics in human-readable format.

isVerified
                  ::  VState -> Bool

Deterministic

Are all non-failing properties verified?

addFailedFuncToStats
                  ::  String -> String -> VState -> VState

Deterministic

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

incNumAllInStats
                  ::  VState -> VState

Deterministic

Increments the number of all tested functions.

incNumNFCInStats
                  ::  VState -> VState

Deterministic

Increments the number of operations with nonfail conditions.

incPatTestInStats
                  ::  VState -> VState

Deterministic

Increments the number of missing pattern tests.

incFailTestInStats
                  ::  VState -> VState

Deterministic

Increments the number of test of posibble failure calls.

addProgToState
                  ::  AProg TypeExpr -> VState -> VState

Deterministic

Adds a new typed FlatCurry program to the state.

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

Deterministic

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 -> [TAProg] -> VState
Fields:
- trInfo :: VerifyInfo
- failedFuncs :: [(String,String)]
- numAllFuncs :: Int
- numNFCFuncs :: Int
- numPatTests :: Int
- numFailTests :: Int
- currTAProgs :: [TAProg]

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 :: VerifyInfo -> VState

Further infos:

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

readVerifyInfoRef :: IORef VState -> IO VerifyInfo

Reads VerifyInfo from VState IORef.

showStats :: VState -> String

Shows the statistics in human-readable format.

isVerified :: VState -> Bool

Are all non-failing properties verified?

Further infos:

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

addFailedFuncToStats :: String -> String -> VState -> VState

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

Further infos:

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

incNumAllInStats :: VState -> VState

Increments the number of all tested functions.

incNumNFCInStats :: VState -> VState

Increments the number of operations with nonfail conditions.

incPatTestInStats :: VState -> VState

Increments the number of missing pattern tests.

incFailTestInStats :: VState -> VState

Increments the number of test of posibble failure calls.

addProgToState :: AProg TypeExpr -> VState -> VState

Adds a new typed FlatCurry program to the state.

Further infos:

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

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

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