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. |
Constructors:
VerifyInfo
:: Options -> [TAFuncDecl] -> [TAFuncDecl] -> [TAFuncDecl] -> [TAFuncDecl] -> VerifyInfo
Fields:
toolOpts
:: Options
allFuncs
:: [TAFuncDecl]
preConds
:: [TAFuncDecl]
postConds
:: [TAFuncDecl]
nfConds
:: [TAFuncDecl]
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]
Type synonym: VStateM a = StateT VState IO a
|
|
Is an operation name the name of a contract or similar? |
Is a function declaration a property? |
|
|
|
|
|
Shows the statistics for the failfree verification in human-readable format. |
Shows the statistics for the contract checking in human-readable format. |
Are all non-failing properties verified?
|
Are all contracts verified?
|
|
Adds a possibly failing call in a functions and the called function. |
Increments the number of all tested functions. |
Increments the number of operations with nonfail conditions. |
Increments the number of missing pattern tests. |
Increments the number of test of possible failure calls. |
Increments the number of preconditions. If the first argument is true, a precondition has been verified. |
Adds an operation to the already processed operations with postconditions. If the second argument is true, the postcondition of this operation has been verified. |
Adds a new typed FlatCurry program to the state. |