Crash when foo() calls Main()

[dnezam]

Dafny version

4.8.0+5faf876b2c768c61044b8f87825385682b6e772d

Code to produce this issue

method Main() {
  print "hello from main";
}

method foo() {
	Main();
}

Command to run and resulting output

Running `dafny run test.dfy` results in

Dafny program verifier finished with 1 verified, 0 errors
Unhandled exception: System.ArgumentOutOfRangeException: Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index')
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrCallStmt(CallStmt s, String receiverReplacement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, ConcreteSyntaxTree wStmtsAfterCall)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrStmtList(List`1 stmts, ConcreteSyntaxTree writer)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileMethod(Program program, Method m, IClassWriter cw, Boolean lookasideBody)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWriter classWriter)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleDefinition module)
   at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.Compile(Program program, ConcreteSyntaxTree wrx)
   at Microsoft.Dafny.ExecutableBackend.Compile(Program dafnyProgram, String dafnyProgramName, ConcreteSyntaxTree output)
   at Microsoft.Dafny.SynchronousCliCompilation.<>c__DisplayClass20_1.<CompileDafnyProgram>b__1()
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
   at Microsoft.Dafny.SynchronousCliCompilation.CompileDafnyProgram(Program dafnyProgram, String dafnyProgramName, ReadOnlyCollection`1 otherFileNames, Boolean invokeCompiler)
   at Microsoft.Dafny.SynchronousCliCompilation.Compile(String fileName, ReadOnlyCollection`1 otherFileNames, Program dafnyProgram, PipelineOutcome oc, IDictionary`2 moduleStats, Boolean verified)
   at Microsoft.Dafny.SynchronousCliCompilation.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId)
   at Microsoft.Dafny.SynchronousCliCompilation.Run(DafnyOptions options)
   at Microsoft.Dafny.RunCommand.<>c.<<Create>b__6_0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass17_0.<<AddDeveloperHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<<UseExceptionHandler>b__0>d.MoveNext()

What happened?

Instead of crashing, I would have expected Dafny to tell me whether this is illegal or not.

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

Linux