fix: Count proof obligations of loop headers #3244
Conversation
There was a problem hiding this comment.
This solves this soundness bug, but now I realize that the mechanism for computing the number of assertions (and emitting nothing if there is no assertion) is stateful, which makes me wonder whether we are missing other cases as well. Isn't there a way that we wouldn't need to manually increment a variable?
|
Yes, it could be stateless. One way to do that would be to generate the entire Boogie procedure implementation and then apply a visitor that checks if there are any proof obligations. Indeed, Boogie could even do that instead of Dafny. It is alarming that the bug that this PR fixes has been around unnoticed for several years. |
|
It appears that the bug was introduced by 2d4176b1 , but this PR isn't reverting the relevant part of that commit (instead it uses a more localized fix). @RustanLeino could you have a second look to check if we might have introduced any other issue not covered by this PR with the original faulty commit? |
This PR changes the verifier to increment the assertion count when it encounters a loop with non-free invariants. This increment was previously missing, which caused certain "loop invariant on entry" checks to be omitted (see dafny-lang#3243). Fixes dafny-lang#3243 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
This PR changes the verifier to increment the assertion count when it encounters a loop with non-free invariants. This increment was previously missing, which caused certain "loop invariant on entry" checks to be omitted (see #3243).
Fixes #3243
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.