-
Notifications
You must be signed in to change notification settings - Fork 266
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
Cycle in type declaration causes crash #4471
Comments
|
Offending file here. Looks like the issue is that the precondition for |
In the commit before fix #4240, public void CheckVariance(Type type, ICallable enclosingTypeDefinition, ...) {
...
} else if (type is UserDefinedType) {
var t = (UserDefinedType)type;
...
} else {
var resolvedClass = t.ResolvedClass;
...
if (lax) {
var cg = enclosingTypeDefinition.EnclosingModule.CallGraph;
var t0 = resolvedClass as ICallable;
if (t0 != null && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative(enclosingTypeDefinition)) {
...
}
}
}
}
} Note that public void CheckVariance(Type type, TopLevelDecl enclosingTypeDefinition, ...) And the innermost if (t0 != null && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative((ICallable)enclosingTypeDefinition))
|
### Description <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix for an issue visible in the latest release? Mention this in the PR details and ensure a patch release is considered --> Fixes #4471, explanation [here](#4471 (comment)). ### How has this been tested? <!-- Tests can be added to `Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to `Source/*.Test/…` and run with `dotnet test` --> Tests under `.../git-issues/git-issue-4471/`. <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> Co-authored-by: Siva Somayyajula <somayyas@amazon.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
…ang#5153) ### Description <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix for an issue visible in the latest release? Mention this in the PR details and ensure a patch release is considered --> Fixes dafny-lang#4471, explanation [here](dafny-lang#4471 (comment)). ### How has this been tested? <!-- Tests can be added to `Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to `Source/*.Test/…` and run with `dotnet test` --> Tests under `.../git-issues/git-issue-4471/`. <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> Co-authored-by: Siva Somayyajula <somayyas@amazon.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Dafny version
current master (post 4.2.0)
Code to produce this issue
Command to run and resulting output
What happened?
The use of
Y
in the type argument to the classY
itself causes Dafny to crash.Note, this crash is rather recent, because the program does not crash with Dafny 4.2.0.
Also note, if this program were accepted (not just without crashing, but without causing any other error), then it is possible that the following program would also be accepted and verified:
This is a variation of
Test/Landin/Knot4.dfy
.What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: