|
definition:
|
verifyFuncCall :: TermDomain a => Expr -> QName -> [Int] -> VerifyStateM a ()
verifyFuncCall exp qf vs = do
opts <- fmap vstToolOpts get
if qf == pre "failed" || (optError opts && qf == pre "error")
then do
bcond <- getExpandedCondition
unsat <- incrNonTrivialCall >> incrUnsatSMT >> isUnsatisfiable bcond
if unsat
then do currfn <- getCurrentFuncName
printIfVerb 3 $ "FUNCTION " ++ snd currfn ++ ": CALL TO " ++
snd qf ++ showArgumentVars vs ++ " NOT REACHABLE\n"
else addFailedFunc exp Nothing fcTrue
else do atype <- getCallType qf (length vs)
if isTotalACallType atype
then return ()
else do mbnfcond <- getNonFailConditionOf qf
verifyNonTrivFuncCall exp qf vs atype mbnfcond
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
-- Verify the abstract type or non-fail condition of a function call.
-- The second argument is the function call as a FlatCurry expression,
-- the third argument is the function name, and the fourth argument
-- are the argument variables.
|
|
indeterministic:
|
might be indeterministic
|
|
infix:
|
no fixity defined
|
|
name:
|
verifyFuncCall
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Analysis.TermDomain.TermDomain a => FlatCurry.Types.Expr -> (String, String)
-> [Prelude.Int]
-> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO ()
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|