Skip to content
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

Crash when "in multiset" in failing precondition #2657

Closed
MikaelMayer opened this issue Aug 30, 2022 · 0 comments · Fixed by #2658
Closed

Crash when "in multiset" in failing precondition #2657

MikaelMayer opened this issue Aug 30, 2022 · 0 comments · Fixed by #2658
Assignees
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) part: verifier Translation from Dafny to Boogie (translator)

Comments

@MikaelMayer
Copy link
Member

MikaelMayer commented Aug 30, 2022

Dafny returns an incorrect error message for this code:

lemma Lemma(x: int, p: multiset<int>)
  requires x in p
{}

method Test() {
  Lemma(1, multiset{});
}

Dafny returns:

git-issue.dfy(6,7): Error: A precondition for this call might not hold.
(0,-1): Related location: This is the precondition that might not hold.

Because the related location is wrong, this also crashes the language server

Unhandled exception. System.UriFormatException: Given uri is null or empty
at OmniSharp.Extensions.LanguageServer.Protocol.DocumentUri.Parse(String value, Boolean strict)
at Microsoft.Dafny.LanguageServer.Language.DiagnosticErrorReporter.CreateLocation(IToken token) in 
@MikaelMayer MikaelMayer added part: verifier Translation from Dafny to Boogie (translator) part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) crash Dafny crashes on this input, or generates malformed code that can not be executed labels Aug 30, 2022
@MikaelMayer MikaelMayer self-assigned this Aug 30, 2022
MikaelMayer added a commit that referenced this issue Aug 30, 2022
Fixes #2657 by adding a token in a generated boogie expression.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) part: verifier Translation from Dafny to Boogie (translator)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant