fix: Crash in the parser. (#2649)

dafny-lang · Aug 30, 2022 · bd28b7d · bd28b7d
1 parent 7161a88
commit bd28b7d
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 2 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -2,6 +2,7 @@
 
 - feat: Support for the `{:opaque}` attibute on `const` (https://github.com/dafny-lang/dafny/pull/2545)
 - feat: Support for plugin-based code actions on the IDE (https://github.com/dafny-lang/dafny/pull/2021)
+- fix: Fixed a crash when parsing `newtype` in the parser (https://github.com/dafny-lang/dafny/pull/2649)
 - fix: Added missing error reporting position on string prefix check (https://github.com/dafny-lang/dafny/pull/2652)
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
 - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
@@ -1492,7 +1492,10 @@ NewtypeDecl<DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td>
        td.StartToken = dmod.FirstToken;
        td.EndToken = t;
     .)
-  )             (. td.TokenWithTrailingDocString = t; .)
+  )  (. if (td != null) {
+          td.TokenWithTrailingDocString = t;
+        }
+     .)
   .
 
 /*------------------------------------------------------------------------*/

diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
@@ -260,3 +260,5 @@ module Older {
   function method C(a: A, ghost older older b: B, nameonly ghost older nameonly ghost c: C := "hello"): int
   twostate lemma L(nameonly older nameonly c: C := "hello") // error: 'older' is an identifier here
 }
+
+newtype T {}
diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect
@@ -79,4 +79,5 @@ ParseErrors.dfy(255,32): Error: formal cannot be declared 'older' in this contex
 ParseErrors.dfy(256,11): Error: formal cannot be declared 'older' in this context
 ParseErrors.dfy(257,17): Error: formal cannot be declared 'older' in this context
 ParseErrors.dfy(261,28): Error: formal cannot be declared 'older' in this context
-76 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(264,10): Error: invalid NewtypeDecl
+77 parse errors detected in ParseErrors.dfy