Exception for Tests with Parameters

[DavePearce]

At the moment, attempting to run tests with parameters generates a rather unhelpful error message (in fact, a stack trace). Example is:

method {:test} broken(x:nat) {
  assert x+1 == x+1;
}

Running this with dafny /runAllTests:1 test.dfy gives the following:

Dafny program verifier finished with 1 verified, 0 errors
Unhandled exception. System.AggregateException: One or more errors occurred. (Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index'))
 ---> 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.SinglePassCompiler.TrCallStmt(CallStmt s, String receiverReplacement, ConcreteSyntaxTree wr)
   at Microsoft.Dafny.Compilers.SinglePassCompiler.TrStmt(Statement stmt, ConcreteSyntaxTree wr)
   at Microsoft.Dafny.Compilers.SinglePassCompiler.TrStmtList(List`1 stmts, ConcreteSyntaxTree writer)
   at Microsoft.Dafny.Compilers.SinglePassCompiler.TrStmt(Statement stmt, ConcreteSyntaxTree wr)
   at Microsoft.Dafny.Compilers.CsharpCompiler.EmitHaltRecoveryStmt(Statement body, String haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr)

Of course, I understand running a test with a parameter perhaps doesn't make sense. But, it perhaps could produce a more useful error message! For reference, my dafny version is 3.7.3.40719.

[robin-aws]

Thanks for the report. There should be logic in the resolver that would reject the test method even without the /runAllTests:1 option. See also #451.

[DavePearce]

Great, thanks Robin. Looks like #451 covers this, so will close it.