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

resolver crash on "as map" #5919

Open
erniecohen opened this issue Nov 16, 2024 · 0 comments
Open

resolver crash on "as map" #5919

erniecohen opened this issue Nov 16, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking

Comments

@erniecohen
Copy link

Dafny version

4.9.0

Code to produce this issue

const z := 0 as map

Command to run and resulting output

No response

What happened?

Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Dafny.CollectionType.<>c.<get_Nodes>b__3_0(Type ta)
at System.Linq.Enumerable.SelectManySingleSelectorIterator2.MoveNext() at System.Linq.Enumerable.ConcatIterator1.MoveNext()
at Microsoft.Dafny.Node.Visit(Func2 beforeChildren, Action1 afterChildren, Action1 reportError) at Microsoft.Dafny.ExpandAtAttributes.PreResolve(Program program) at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<<Resolve>b__0>d.MoveNext() --- End of stack trace from previous location --- at Microsoft.Dafny.PruneIfNotUsedSinceLastPruneCache2.UseAndPrune[T](Func1 use, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,TKey,TValue](PruneIfNotUsedSinceLastPruneCache2 cache, Func`1 useCache, ILogger logger, TelemetryPublisherBase telemetryPublisher, String programName, String activity, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.ResolveAsync()
at Microsoft.Dafny.Compilation.LogExceptions()

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 Nov 16, 2024
@robin-aws robin-aws added the part: resolver Resolution and typechecking label Nov 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
Projects
None yet
Development

No branches or pull requests

2 participants