-
Notifications
You must be signed in to change notification settings - Fork 260
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Dafny reports verification error twice #2703
Comments
I see the verification of the wellformedness of Absy.Foo is done twice. Is that required for soundness? I have trouble overseeing the implication of the |
Here is a variant of this same issue, which shows that it's not restricted to imports:
This produces the following output:
For this variant, however, we did not use to print two errors until very recently; that bug was introduced in 3.7.2. The problem in the original post:
reports two errors in every version of Dafny that can parse it. I don't think it should: module verification is supposed to be modular, so I don't see why we're re-checking well-formedness :/ |
Defensive programming. Reduces the impact of #2703 while we work on fixing it. <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>
I agree that there should be no need to verify this twice. I don't know how come we do. This is how these things are generally performed: There are two cases when we make a refinement clone of a module--when you say So, perhaps what's going wrong in the report bug is that the |
Reports:
Note the double "possible division by zero"
Also note that this program causes an exception in the Dafny language server:
The text was updated successfully, but these errors were encountered: