Internal Error: System.NullReferenceException

[erniecohen]

Dafny version

4.6.0 (nightly 4/17)

Code to produce this issue

trait Ins {
    function step(s:State):State //requires safe?(s)
}
type Code = seq<Ins>
datatype State = S(
    clock:nat
) {
    function fetch_():Ins
    const fetch := fetch_()
    const step := fetch.step(this)
    function run():State decreases clock {
        if clock == 0 then this else step.(clock := clock - 1).run()
    }
}

Command to run and resulting output

vscode (resolving)

What happened?

System.NullReferenceException: Object reference not set to an instance of an object.\n at Microsoft.Dafny.ConcreteSyntaxExpression.get_TerminalExpressions()+MoveNext()\n at System.Linq.Enumerable.All[TSource](IEnumerable1 source, Func2 predicate)\n at Microsoft.Dafny.ExpressionTester.CheckIsCompilable(Expression expr, ICodeContext codeContext, Boolean insideBranchesOnly)\n at Microsoft.Dafny.ModuleResolver.ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl)\n at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List1 declarations, Graph1 datatypeDependencies, Graph1 codatatypeDependencies, String moduleDescription, Boolean isAnExport)\n at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName)\n at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)\n at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)\n at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)\n at Microsoft.Dafny.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)\n at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)\n at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>n__0(CancellationToken cancellationToken)\n at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<Resolve>b__0()\n at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,Key,Value](PruneIfNotUsedSinceLastPruneCache2 cache, Func`1 useCache, TelemetryPublisherBase telemetryPublisher, String programName, String activity)\n at Microsoft.Dafny.LanguageServer.Language.CachingResolver.Resolve(CancellationToken cancellationToken)\n at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)\n at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)\n at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)\n at Microsoft.Dafny.TextDocumentLoader.<>c__DisplayClass5_0.<<ResolveAsync>b__0>d.MoveNext()\n--- End of stack trace from previous location ---\n at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)\n at Microsoft.Dafny.Compilation.ResolveAsync()", "startLineNumber": 1, "startColumn": 1, "endLineNumber": 1, "endColumn": 2 }]

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

Mac

[MikaelMayer]

This is a bug in the new resolver. I was able to reproduce it. The old resolver did not have this issue.