CurryInfo: contract-prover-4.0.0 / ContractProver.proveContractsInProg

 
proveContractsInProg :: Options -> TAProg ->  IO ()
proveContractsInProg opts oprog = do
  let sprog = simpProg oprog
  printWhenAll opts $ unlines $
    ["ORIGINAL PROGRAM:",   line, showCurryModule (unAnnProg oprog), line,
     "SIMPLIFIED PROGRAM:", line, showCurryModule (unAnnProg sprog), line]
  vstref <- newIORef (initVState (makeVerifyInfo opts (progFuncs sprog)))
  modifyIORef vstref (addProgToState sprog)
  prog1 <- verifyPostConditions opts oprog vstref
  prog2 <- verifyPreConditions  opts prog1 vstref
  prog3 <- addPreConditions     opts prog2 vstref
  let unewprog = unAnnProg prog3
      mname    = progName prog3
  printWhenAll opts $ unlines $
    ["TRANSFORMED PROGRAM WITH CONTRACT CHECKING:", line,
     showCurryModule unewprog, line]
  vst2 <- readIORef vstref
  when (areContractsAdded vst2) $ do
    when (optFCY opts) $
      writeTransformedFCY opts (flatCurryFileName mname) unewprog
    when (optTAFCY opts) $
      writeTransformedTAFCY opts (typeAnnotatedFlatCurryFileName mname) prog3
  printWhenStatus opts (showStats vst2)
 where
  line = take 78 (repeat '-')

 no demanded arguments

 deterministic operation

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_) |-> _}

 proveContractsInProg

 no precedence defined

 _

 ToolOptions.Options -> FlatCurry.Annotated.Types.AProg FlatCurry.Types.TypeExpr
-> Prelude.IO ()

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term