Dafny crashing when revealing a non-static class method from outside the class

[EkanshdeepGupta]

Dafny version

4.1.0

Code to produce this issue

// class_test.dfy :

method test() {
    var c := new Class();
    reveal Class.P();
    assert c.P();
}

class Class {
  opaque function P() : bool { true }

  constructor () { }
}

Command to run and resulting output

dafny verify class_test.dfy

What happened?

Upon running the above, Dafny is crashing with the following output:

% dafny verify ./test/class_test.dfy
/Users/ekanshdg/test/class_test.dfy(3,17): Error: accessing member 'reveal_P' requires an instance expression
/Users/ekanshdg/test/class_test.dfy(3,11): Error: call to instance method requires an instance
Unhandled exception. System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.CallStmt.get_NonSpecificationSubExpressions()+MoveNext() in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/AST/Statements/CallStmt.cs:line 73
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 923
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass17_0.<Traverse>b__2(Statement subStmt) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 925
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 923
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass17_0.<Traverse>b__2(Statement subStmt) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 925
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 923
   at Microsoft.Dafny.ProgramTraverser.Traverse(MemberDecl memberDeclaration, String field, Object parent) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 905
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass15_0.<Traverse>b__0(MemberDecl memberDecl) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 779
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(TopLevelDecl topd) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 779
   at Microsoft.Dafny.ProgramTraverser.Traverse(List`1 topLevelDecls) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Generic/Util.cs:line 720
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleName, Boolean isAnExport) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Resolver/Resolver.cs:line 2928
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Resolver/Resolver.cs:line 833
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/Resolver/Resolver.cs:line 534
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/DafnyMain.cs:line 266
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyCore/DafnyMain.cs:line 216
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyDriver/DafnyDriver.cs:line 403
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyDriver/DafnyDriver.cs:line 124
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0() in /private/tmp/dafny-20230511-13185-uupd2y/dafny-4.1.0/Source/DafnyDriver/DafnyDriver.cs:line 102
   at System.Threading.Thread.StartCallback()

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

Mac

[MikaelMayer]

Related
#2689 (comment)