CurryInfo: contract-prover-4.0.0 / ContractProver.verifyPreConditions

 
verifyPreConditions :: Options -> TAProg -> IORef VState -> IO TAProg
verifyPreConditions opts prog vstref = do
  newfuns  <- mapM (provePreCondition opts vstref) (progFuncs prog)
  return (updProgFuncs (const newfuns) prog)

 no demanded arguments

 deterministic operation

 
------------------------------------------------------------------------
Try to verify preconditions: If an operation `f` occurring in some
right-hand side has a precondition, a proof for the validity of
this precondition is extracted.
If the proof is not successful, a precondition check is added to this call.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_,_) |-> _}

 verifyPreConditions

 no precedence defined

 _

 ToolOptions.Options -> FlatCurry.Annotated.Types.AProg FlatCurry.Types.TypeExpr
-> Data.IORef.IORef VerifierState.VState
-> Prelude.IO (FlatCurry.Annotated.Types.AProg FlatCurry.Types.TypeExpr)

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term