Add optional file path for verify to write SMTLib2 output
#1100
Conversation
rsoeldner
force-pushed
the
verify-debug
branch
from
522f466 to
08ad767
Compare
There was a problem hiding this comment.
I like the idea! Suggesting a small change in scope here to reduce complexity: the convention for debugging output in natives is a Boolean flag overload. In keeping with that, it may be good to just choose a dedicated dotfile into which we can just dump smt output if the flag is set to true. We already have a notion of .pact-history. I'm proposing .pact-verify-{module name} or some variation of that instead of having the user supply an absolute or relative path.
| @@ -452,23 +451,26 @@ verifyFunctionInvariants tf (CheckEnv tables _consts _pDefs moduleData caps gov | |||
| catchingExceptions act = act `E.catch` \(e :: SBV.SBVException) -> | |||
| pure $ Left $ CheckFailure funInfo $ SmtFailure $ UnexpectedFailure e | |||
|
|
|||
| modName = moduleDefName $ _mdModule moduleData | |||
|
|
|||
| debugFile = if debug then Just $ ".pact-verify-"<> asString' modName else Nothing | |||
There was a problem hiding this comment.
As a note, asString uses the namespace prefixed module name.
There was a problem hiding this comment.
@jmcardon , I need to write to several temporary files for this feature. Is there any policy/library/functions in-place within pact?
There was a problem hiding this comment.
I don't believe so, but I think this should be doable with System.FilePath+ io bracket.
|
closed in favour of #1122 |
Add optional parameter to
verifyallowing to inspect generated SMTLib2 file (by SBV).