KiCS2
Exported names: 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 :: VerifyInfo -> VState   
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?
addFailedFuncToStats :: String -> String -> VState -> VState   
Adds a possibly failing call in a functions and the called function.
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.
tdeclOf :: VState -> (String,String) -> Maybe TypeDecl   
Selects the type declaration of a type constructor from the state.

Exported datatypes:

VerifyInfo

Constructors:

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

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.