-
Notifications
You must be signed in to change notification settings - Fork 256
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 verifies program with NPE #1377
Comments
keyboardDrummer
pushed a commit
that referenced
this issue
Aug 25, 2021
Previously, the type-equality checks for overriding methods/functions ignored type constraints. With this PR, the proper type equality is used. Note, one can imagine allowing some co-/contra-variance among the parameters in an override. That would indeed be sound, but it may cause complications in compilation, since target languages may have different rules. Therefore, I suggest we continue to insist on type equality in Dafny. If a strong need for co-/contra-variance comes up, we can consider changing the language. Fixes #1377
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The following program verifies and crashes with a NPE:
The text was updated successfully, but these errors were encountered: