Skip to content

v2.13.3

@MikaelMayer MikaelMayer tagged this 23 Mar 20:15
Enables Boogie to report in real-time its current execution state.
Specifically, enable the output printers to
* `ReportImplementationsBeforeVerification`: Be notified about the implementations to be verified, for example to change priorities on the fly
* `ReportStartVerifyImplementation`: Be notified when an implementation starts to verify
* `ReportEndVerifyImplementation`: Be notified when an implementation finishes to verify
* `ReportSplitResult`: Be notified when an split finishes
  * There are three places in which I needed to call this: 1) When the prover did not fail, 2) When the prover returns a time out and it was the last change to split the assertions 3) When there is no way it can split the assertions further
  * I changed `VCResult` a bit so that stores the counter-examples obtained from the split itself.
  * I added a method to `VCResult` so that it can compute per-assert outcomes and counter-examples, if any.
* I fixed all the tests on Windows as well (a log file was not closed before being accessed, as a null pointer exception that was throwing because Process was null)
* I added a test for the new behavior of the `OutputPrinter`

** Breaking change** The output printer's interface is changed.
Assets 2
Loading