dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

resolver crash on "as map" #5919

Open erniecohen opened 6 days ago

erniecohen commented 6 days ago

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.b3_0(Type ta) at System.Linq.Enumerable.SelectManySingleSelectorIterator2.MoveNext() at System.Linq.Enumerable.ConcatIterator1.MoveNext() at Microsoft.Dafny.Node.Visit(Func2 beforeChildren, Action1 afterChildren, Action`1 reportError) at Microsoft.Dafny.ExpandAtAttributes.PreResolve(Program program) at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<b0>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, Func1 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