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

internal error when f.Keys is used to define a const field Keys of a datatype #4394

Closed
erniecohen opened this issue Aug 6, 2023 · 0 comments · Fixed by #4423
Closed

internal error when f.Keys is used to define a const field Keys of a datatype #4394

erniecohen opened this issue Aug 6, 2023 · 0 comments · Fixed by #4423
Assignees
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)

Comments

@erniecohen
Copy link

erniecohen commented Aug 6, 2023

Dafny version

4.2.0

Code to produce this issue

datatype T = T(
    f:map<nat,nat>
) {
    const Keys := f.Keys. // no problem if another name is used for the constant
}

Command to run and resulting output

vscode

What happened?

Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.InferredTypeProxy' to type 'Microsoft.Dafny.SetType'.
at Microsoft.Dafny.Translator.GetReadonlyField(Field f)
at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
at Microsoft.Dafny.Translator.AddRevealableTypeDecl(RevealableTypeDecl d)
at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule)
at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext()
at System.Collections.Generic.List1..ctor(IEnumerable1 collection)
at System.Linq.Enumerable.ToList[TSource](IEnumerable1 source) at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass4_0.<GetVerificationTasksAsync>b__1() at System.Threading.Tasks.Task1.InnerInvoke()
at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(CompilationAfterResolution compilation, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.PrepareVerificationTasksAsync(CompilationAfterResolution loaded, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.TranslateAsync()

What type of operating system are you experiencing the problem on?

Mac

@erniecohen erniecohen added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Aug 6, 2023
@erniecohen erniecohen changed the title internal error internal error when f.Keys is used to define a const field Keys of a datatype Aug 6, 2023
@atomb atomb added part: verifier Translation from Dafny to Boogie (translator) crash Dafny crashes on this input, or generates malformed code that can not be executed labels Aug 7, 2023
MikaelMayer added a commit that referenced this issue Aug 15, 2023
@MikaelMayer MikaelMayer self-assigned this Aug 17, 2023
MikaelMayer added a commit that referenced this issue Aug 29, 2023
…4423)

This PR fixes #4394
I added the corresponding test.

<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: Rustan Leino <leino@amazon.com>
keyboardDrummer pushed a commit to keyboardDrummer/dafny that referenced this issue Sep 15, 2023
…afny-lang#4423)

This PR fixes dafny-lang#4394
I added the corresponding test.

<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: Rustan Leino <leino@amazon.com>
keyboardDrummer pushed a commit that referenced this issue Sep 19, 2023
…4423)

This PR fixes #4394
I added the corresponding test.

<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: Rustan Leino <leino@amazon.com>
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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants