-
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
Fix: null pointer exception in the case of hovering local variables #2437
Conversation
…hat were duplicated but not with their type.
Source/DafnyLanguageServer/Language/Symbols/FormatExtensions.cs
Outdated
Show resolved
Hide resolved
@@ -12002,7 +12002,8 @@ private class RBranchExpr : RBranch { | |||
// deep clone Patterns and Body |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm somewhat hesitant about this change. We should probably come up with a different name and comment, if you really just want to clone part of it. What about CloneRBranchExpr
? Also, the tests fail.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes :-(
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm somewhat hesitant about this change. We should probably come up with a different name and comment, if you really just want to clone part of it. What about
CloneRBranchExpr
? Also, the tests fail.
I just pushed a more conservative version of the changes which prevent local variables from being cloned if their type
is not yet assigned, that way, any type assigned later on a local variable of a cloned tree will make the original local variable (which is the same) have the same type.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's still not clear to me that this is safe. Couldn't we re-infer the type on all branches? Would you mind soliciting someone else's review?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, that's fair to ask. I'm very much puzzled by the code that deals with nested match statements. Let me ask @RustanLeino
Source/Dafny/Resolver.cs
Outdated
return new RBranchStmt(branch.Tok, branch.BranchID, | ||
branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), new List<Statement>(branch.Body), cloner.CloneAttributes(branch.Attributes)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
return new RBranchStmt(branch.Tok, branch.BranchID, | |
branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), new List<Statement>(branch.Body), cloner.CloneAttributes(branch.Attributes)); | |
return new RBranchStmt(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), | |
new List<Statement>(branch.Body), cloner.CloneAttributes(branch.Attributes)); |
Co-authored-by: Fabio Madge <[email protected]>
Source/DafnyLanguageServer/Language/Symbols/FormatExtensions.cs
Outdated
Show resolved
Hide resolved
Co-authored-by: Fabio Madge <[email protected]>
Reverted the output of 1665
Is the following correct? The user hovers over the local variable, then the language server finds the cloned variable. The cloned variable at that time has no The way |
If by "cloned variable" you mean "the original variable before it was cloned", then your interpretation is correct.
It's the second time that I observe that the sugared match does not have I think your approach for the LSP would work (to look up for the desugared version and collect symbols there instead of the original |
This may be okay for now. We've seen several issues with the fact that the desugaring happens here (as opposed to keeping the original "nested" match), so I predict we'll rewrite this in the near future. |
# Conflicts: # RELEASE_NOTES.md
Fixes #2438
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.