Properly check if types may contain references #1924
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
cpitclaudel
previously approved these changes
Mar 22, 2022
There was a problem hiding this comment.
For datatypes, why is it enough to check just the type parameters? The following looks off to me:
class C {}
datatype D = DC(c: C)
type X(!new) = D // No error
datatype Obs' = Obs'(s: set<object>)
predicate lotsOfObjects'() {
exists o: Obs' :: |o.s| > 10 // No error
}
And also this:
class C {}
datatype Box<T> = Box(t: T)
type Box'(!new) = Box<C> // Rejected
datatype BoxC = BoxC(c: C)
type BoxC'(!new) = BoxC // No error
Am I missing something?
|
@cpitclaudel Thank you. These are (still) bugs. |
|
Do we adress them in the same PR, or merge this one and open a separate ticket for the next? |
The Schorr-Waite test programs are not allowed by the new rules. To sort this out, Dafny needs a more flexible mechanism to indicate that quantifiers only quantify over allocated state. I will add this mechanism in a separate PR and then return to this one.
|
@cpitclaudel I addressed the further issues in this PR with the commit I just pushed. However, the fix causes errors that the old Schorr-Waite test programs have a function that depends on the allocation state. To sort this out, Dafny needs a more flexible mechanism to indicate that quantifiers only quantify over allocated state. I will add this mechanism in a separate PR and then return to this one. |
These `:older` attributes on `ReachableVia` will once again allow the `SchorrWaite*.dfy` tests, as soon as dafny-lang#1936 is merged.
cpitclaudel
requested changes
Mar 28, 2022
# Conflicts: # RELEASE_NOTES.md
# Conflicts: # RELEASE_NOTES.md # Source/Dafny/Resolver.cs
cpitclaudel
approved these changes
Apr 28, 2022
cpitclaudel
added a commit
that referenced
this pull request
May 4, 2022
The new check is correct, but this is not fully satisfactory, as it removes a useful debugging aid. Ideally, it would be nice to be able to mark these extern classes as frozen, so that they might be treated as `!new`.
cpitclaudel
added a commit
to dafny-lang/compiler-bootstrap
that referenced
this pull request
Jun 28, 2022
The new check is correct, but this is not fully satisfactory, as it removes a useful debugging aid. Ideally, it would be nice to be able to mark these extern classes as frozen, so that they might be treated as `!new`.
cpitclaudel
added a commit
to dafny-lang/compiler-bootstrap
that referenced
this pull request
Jul 12, 2022
The new check is correct, but this is not fully satisfactory, as it removes a useful debugging aid. Ideally, it would be nice to be able to mark these extern classes as frozen, so that they might be treated as `!new`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Previously, types were not properly checked for whether or not they may contain references. This PR fixes that.
Fixes #1419
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.