Module VerifierState

Summary of exported operations:

makeTransInfo :: Options -> [AFuncDecl TypeExpr] -> TransInfo   
initVState :: TransInfo -> VState   
readTransInfoRef :: IORef VState -> IO TransInfo   
Reads TransInfo 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.

Exported datatypes:


TransInfo

Constructors:


VState

Constructors:

  • VState :: TransInfo -> [String] -> [String] -> [String] -> [String] -> [AProg TypeExpr] -> VState

    Fields:

    • trInfo :: TransInfo
    • uPreCond :: [String]
    • vPreCond :: [String]
    • uPostCond :: [String]
    • vPostCond :: [String]
    • currTAProgs :: [AProg TypeExpr]

Exported operations:

initVState :: TransInfo -> VState   

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

readTransInfoRef :: IORef VState -> IO TransInfo   

Reads TransInfo 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