Module VerifierState

Summary of exported operations:

makeVerifyInfo :: Options -> [AFuncDecl TypeExpr] -> VerifyInfo  Deterministic 
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.
areContractsAdded :: VState -> Bool  Deterministic 
Is the program transformed so that some contracts are added?
addPreCondToStats :: String -> Bool -> VState -> VState  Deterministic 
Increments the number of preconditions.
addPostCondToStats :: String -> Bool -> VState -> VState  Deterministic 
Adds an operation to the already processed operations with postconditions.
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:

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:

initVState :: VerifyInfo -> VState  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

readVerifyInfoRef :: IORef VState -> IO VerifyInfo  Deterministic 

Reads VerifyInfo from VState IORef.

showStats :: VState -> String  Deterministic 

Shows the statistics in human-readable format.

areContractsAdded :: VState -> Bool  Deterministic 

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  Deterministic 

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

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

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  Deterministic 

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  Deterministic 

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