| definition: |
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 '-')
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,_) |-> _}
|
| name: |
proveContractsInProg |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
ToolOptions.Options -> FlatCurry.Annotated.Types.AProg FlatCurry.Types.TypeExpr -> Prelude.IO () |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |