Module VerifierState

Summary of exported operations:

makeVerifyInfo
                  ::  Options -> [AFuncDecl TypeExpr] -> VerifyInfo

initVState
                  ::  VerifyInfo -> VState

readVerifyInfoRef
                  ::  IORef VState -> IO VerifyInfo

Reads VerifyInfo from VState IORef.

showStats
                  ::  VState -> String

Shows the statistics in human-readable format.

areContractsAdded
                  ::  VState -> Bool

Is the program transformed so that some contracts are added?

addPreCondToStats
                  ::  String -> Bool -> VState -> VState

Increments the number of preconditions.

addPostCondToStats
                  ::  String -> Bool -> VState -> VState

Adds an operation to the already processed operations with postconditions.

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:

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

VState

Constructors:

VState :: VerifyInfo -> [String] -> [String] -> [String] -> [String] -> [TAProg] -> VState
Fields:
- trInfo :: VerifyInfo
- uPreCond :: [String]
- vPreCond :: [String]
- uPostCond :: [String]
- vPostCond :: [String]
- currTAProgs :: [TAProg]

Exported operations:

makeVerifyInfo :: Options -> [AFuncDecl TypeExpr] -> VerifyInfo

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.

areContractsAdded :: VState -> Bool

Is the program transformed so that some contracts are added?

Further infos:

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

addPreCondToStats :: String -> Bool -> VState -> VState

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

addPostCondToStats :: String -> Bool -> VState -> VState

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

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.