dafny-lang / dafny

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

NullReferenceException in SkeletonStatement.SubStatements #1927

Open cpitclaudel opened 2 years ago

cpitclaudel commented 2 years ago

The following code snippet crashes Dafny:

method Abs(x: int) returns (y: int) { ...; }
tmp.dfy(3,3): Error: skeleton statements are allowed only in refining methods
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.SkeletonStatement.get_SubStatements()+MoveNext() in .\git\dafny\master\Source\Dafny\AST\DafnyAst.cs:line 8918
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in .\git\dafny\master\Source\Dafny\Util.cs:line 747
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass17_0.<Traverse>b__2(Statement subStmt) in .\git\dafny\master\Source\Dafny\Util.cs:line 749
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(Statement stmt, String field, Object parent) in .\git\dafny\master\Source\Dafny\Util.cs:line 747
   at Microsoft.Dafny.ProgramTraverser.Traverse(MemberDecl memberDeclaration, String field, Object parent) in .\git\dafny\master\Source\Dafny\Util.cs:line 729
   at Microsoft.Dafny.ProgramTraverser.<>c__DisplayClass15_0.<Traverse>b__0(MemberDecl memberDecl) in .\git\dafny\master\Source\Dafny\Util.cs:line 603
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.ProgramTraverser.Traverse(TopLevelDecl topd) in .\git\dafny\master\Source\Dafny\Util.cs:line 603
   at Microsoft.Dafny.ProgramTraverser.Traverse(List`1 topLevelDecls) in .\git\dafny\master\Source\Dafny\Util.cs:line 544
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in .\git\dafny\master\Source\Dafny\Resolver.cs:line 3533
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in .\git\dafny\master\Source\Dafny\Resolver.cs:line 1022
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in .\git\dafny\master\Source\Dafny\Resolver.cs:line 497
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in .\git\dafny\master\Source\Dafny\DafnyMain.cs:line 161
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in .\git\dafny\master\Source\Dafny\DafnyMain.cs:line 112
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(ExecutionEngineOptions options, IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in .\git\dafny\master\Source\DafnyDriver\DafnyDriver.cs:line 241
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in .\git\dafny\master\Source\DafnyDriver\DafnyDriver.cs:line 57
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1_0.<Main>b__0() in .\git\dafny\master\Source\DafnyDriver\DafnyDriver.cs:line 37
   at System.Threading.Thread.StartCallback()
Ao-senXiong commented 2 weeks ago

I can not reproduce the issue using cli or master branch. @MikaelMayer do you have any suggestion on how to reproduce it or this issue is somehow fixed?

➜  dafny git:(master) ✗ dafny --version   
4.8.1
➜  dafny git:(master) ✗ dafny run demo.dfy
demo.dfy(1,41): Warning: the ... refinement feature in statements is deprecated
  |
1 | method Abs(x: int) returns (y: int) { ...; }
  |                                          ^

demo.dfy(1,38): Error: skeleton statements are allowed only in refining methods
  |
1 | method Abs(x: int) returns (y: int) { ...; }
  |                                       ^^^

1 resolution/type errors detected in demo.dfy

➜  dafny git:(master) ✗ Scripts/dafny run demo.dfy              
demo.dfy(1,41): Warning: the ... refinement feature in statements is deprecated
  |
1 | method Abs(x: int) returns (y: int) { ...; }
  |                                          ^

demo.dfy(1,38): Error: skeleton statements are allowed only in refining methods
  |
1 | method Abs(x: int) returns (y: int) { ...; }
  |                                       ^^^

1 resolution/type errors detected in demo.dfy