Module Main

banner :: String   

main :: IO ()   

verifyModuleIfNew :: TermDomain a => Analysis a -> IORef ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> IO ()   

Verify a single module if necessary, i.e., not previously verified.

verifyModule :: TermDomain a => Analysis a -> IORef ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> Prog -> IO ()   

Verify a single module.

inferCallTypes :: TermDomain a => Options -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> ((String,String) -> Bool) -> String -> ClockTime -> Prog -> Maybe [((String,String),Maybe [a])] -> IO ([((String,String),Maybe [a])],Int,Int)   

Infer the initial (abstract) call types of all functions in a program and return them together with the number of all/public non-trivial call types. The last argument are the already stored old call types, if they are up to date.

inferIOTypes :: TermDomain a => Options -> Analysis a -> IORef (AnalysisStore a) -> ((String,String) -> Bool) -> Prog -> IO ([((String,String),InOutType a)],Int,Int)   

Infer the in/out types of all functions in a program and return them together with the number of all and public non-trivial in/out types.

showFunctionInfo :: TermDomain a => Options -> String -> VerifyState a -> IO ()   

tryVerifyProg :: TermDomain a => Options -> Int -> VerifyState a -> String -> Map (String,String) [FuncDecl] -> [FuncDecl] -> IO (Int,VerifyState a)   

printVerifyResult :: TermDomain a => Options -> VerifyState a -> String -> ((String,String) -> Bool) -> IO ()   

Prints a message about the result of the module verification.

printVerifyResults :: TermDomain a => Options -> String -> ((String,String) -> Bool) -> [FuncDecl] -> [((String,String),Maybe [a])] -> [((String,String),([(Int,TypeExpr)],Expr))] -> IO ()   

Further infos:

• partially defined

showIncompleteBranch :: (String,String) -> Expr -> [(String,String)] -> String   

initVerifyState :: TermDomain a => IORef ProgInfo -> Prog -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> Map (String,String) (Maybe [a]) -> Map (String,String) ([(Int,TypeExpr)],Expr) -> Map (String,String) (Maybe [a]) -> Map (String,String) (InOutType a) -> [((String,String),([(Int,TypeExpr)],Expr))] -> Options -> IO (VerifyState a)   

Initializes the verification state.

setToolError :: TermDomain a => StateT (VerifyState a) IO ()   

currentFuncDecls :: TermDomain a => VerifyState a -> IO [FuncDecl]   

setCurrentFunc :: TermDomain a => (String,String) -> Int -> [Int] -> StateT (VerifyState a) IO ()   

getCurrentFuncName :: TermDomain a => StateT (VerifyState a) IO (String,String)   

getConsInfos :: TermDomain a => StateT (VerifyState a) IO [((String,String),(Int,ConsType,[((String,String),Int)]))]   

setFreshVarIndex :: TermDomain a => Int -> StateT (VerifyState a) IO ()   

newFreshVarIndex :: TermDomain a => StateT (VerifyState a) IO Int   

addCallTypeRestriction :: TermDomain a => (String,String) -> Maybe [a] -> StateT (VerifyState a) IO ()   

addConditionRestriction :: TermDomain a => (String,String) -> Expr -> StateT (VerifyState a) IO ()   

setNewFunCondition :: TermDomain a => (String,String) -> ([(Int,TypeExpr)],Expr) -> StateT (VerifyState a) IO ()   

Sets a new non-fail condition for a function. If the function has already a new non-fail condition, they will be combined.

aCallType2Bool :: TermDomain a => [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [Int] -> Maybe [a] -> Expr   

Tries to generate a Boolean condition from an abstract call type, if possible.

addFailedFunc :: TermDomain a => Expr -> Maybe [(Int,a)] -> Expr -> StateT (VerifyState a) IO ()   

addMissingCase :: TermDomain a => Expr -> [(String,String)] -> StateT (VerifyState a) IO ()   

getVarExps :: TermDomain a => StateT (VerifyState a) IO [(Int,TypeExpr,Expr)]   

setVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> StateT (VerifyState a) IO ()   

setVarExpTypeOf :: TermDomain a => Int -> TypeExpr -> StateT (VerifyState a) IO ()   

addVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> StateT (VerifyState a) IO ()   

getVarTypes :: TermDomain a => StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]   

getVarTypeOf :: TermDomain a => Int -> StateT (VerifyState a) IO [(InOutType a,[Int])]   

setVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO ()   

addVarType :: TermDomain a => Int -> [(InOutType a,[Int])] -> StateT (VerifyState a) IO ()   

addVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO ()   

addVarAnyType :: TermDomain a => Int -> StateT (VerifyState a) IO ()   

removeVarAnyType :: TermDomain a => Int -> StateT (VerifyState a) IO ()   

getCondition :: TermDomain a => StateT (VerifyState a) IO (Expr -> Expr)   

getExpandedCondition :: TermDomain a => StateT (VerifyState a) IO Expr   

getExpandedConditionWithConj :: TermDomain a => Expr -> StateT (VerifyState a) IO Expr   

setCondition :: TermDomain a => (Expr -> Expr) -> StateT (VerifyState a) IO ()   

setCallCondition :: TermDomain a => Expr -> StateT (VerifyState a) IO ()   

addConjunct :: TermDomain a => Expr -> StateT (VerifyState a) IO ()   

addSingleCase :: TermDomain a => Int -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()   

addEquVarCondition :: TermDomain a => Int -> Expr -> StateT (VerifyState a) IO ()   

getNonFailConditionOf :: TermDomain a => (String,String) -> StateT (VerifyState a) IO (Maybe ([(Int,TypeExpr)],Expr))   

getCallType :: TermDomain a => (String,String) -> Int -> StateT (VerifyState a) IO (Maybe [a])   

getFuncType :: TermDomain a => (String,String) -> Int -> StateT (VerifyState a) IO (InOutType a)   

Further infos:

• partially defined

incrNonTrivialCall :: TermDomain a => StateT (VerifyState a) IO ()   

incrIncompleteCases :: TermDomain a => StateT (VerifyState a) IO ()   

incrUnsatSMT :: TermDomain a => StateT (VerifyState a) IO ()   

getToolOptions :: TermDomain a => StateT (VerifyState a) IO Options   

printIfVerb :: TermDomain a => Int -> String -> StateT (VerifyState a) IO ()   

Prints a string with putStrLn if the verbosity is at least as the given one.

verifyFunc :: TermDomain a => FuncDecl -> StateT (VerifyState a) IO ()   

noVerifyFunctions :: [(String,String)]   

Further infos:

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

verifyFuncRule :: TermDomain a => [Int] -> TypeExpr -> Expr -> StateT (VerifyState a) IO ()   

showVarExpTypes :: TermDomain a => StateT (VerifyState a) IO ()   

verifyExpr :: TermDomain a => Bool -> Expr -> StateT (VerifyState a) IO Int   

verifyVarExpr :: TermDomain a => Int -> Expr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]   

verifyFuncCall :: TermDomain a => Expr -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()   

verifyNonTrivFuncCall :: TermDomain a => Expr -> (String,String) -> [Int] -> Maybe [a] -> Maybe ([(Int,TypeExpr)],Expr) -> StateT (VerifyState a) IO ()   

checkPredefinedOp :: TermDomain a => Expr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]   

verifyMissingBranches :: TermDomain a => Expr -> Int -> [BranchExpr] -> StateT (VerifyState a) IO ()   

getBranchState :: TermDomain a => StateT (VerifyState a) IO ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr)   

restoreBranchState :: TermDomain a => ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr) -> StateT (VerifyState a) IO ()   

verifyBranch :: TermDomain a => Int -> Int -> BranchExpr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]   

getVarType :: TermDomain a => Int -> [(Int,[(InOutType a,[Int])])] -> a   

funcDecls2Usage :: String -> [FuncDecl] -> Map (String,String) [FuncDecl]   

Computes for a given set of function declarations in a module a mapping from module function names to the list of function declarations where these names are used in the right-hand side.

unionFDecls :: [FuncDecl] -> [FuncDecl] -> [FuncDecl]   

usedFuncsInFunc :: FuncDecl -> [(String,String)]   

Get function names used in the right-hand side of a function declaration.

usedFuncsInRule :: Rule -> [(String,String)]   

Get function names used in the right-hand side of a rule.

anyTypes :: TermDomain a => Int -> [a]   

A list of any types of a given length.

enforceNormalForm :: Options -> String -> a -> IO ()   

Further infos:

• partially defined

showSimpExp :: Expr -> String   

isUnsatisfiable :: TermDomain a => Expr -> StateT (VerifyState a) IO Bool   

Checks the unsatisfiability of a Boolean expression w.r.t. a set of variables (second argument) with an SMT solver.