fix: Crash when compiling an empty source file while including testin…

…g code

Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs

@@ -17,13 +17,15 @@ void ObjectInvariant() {
 
   public override IToken Tok {
     get {
-      var previous = Rhs.StartToken.Prev;
-      // If there was a single assignment, report on the operator.
-      var singleAssignment = previous.val == ":=";
-      // If there was an implicit return assignment, report on the return.
-      var implicitAssignment = previous.val == "return";
-      if (singleAssignment || implicitAssignment) {
-        return previous;
+      if (Rhs.StartToken.Prev is not null) {
+        var previous = Rhs.StartToken.Prev;
+        // If there was a single assignment, report on the operator.
+        var singleAssignment = previous.val == ":=";
+        // If there was an implicit return assignment, report on the return.
+        var implicitAssignment = previous.val == "return";
+        if (singleAssignment || implicitAssignment) {
+          return previous;
+        }
       }
       return Rhs.StartToken;
     }

Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs

@@ -93,7 +93,7 @@ internal override void PreResolve(Program program) {
   /// }
   /// </summary>
   internal override void PostResolve(Program program) {
-    var tok = program.GetStartOfFirstFileToken();
+    var tok = program.GetStartOfFirstFileToken() ?? Token.NoToken;
     List<Statement> mainMethodStatements = new();
     var idGenerator = new FreshIdGenerator();
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy

@@ -0,0 +1,2 @@
+// RUN: %translate cs --include-test-runner --allow-warnings %s > "%t"
+// RUN: %diff "%s.expect" "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy.expect

@@ -0,0 +1,7 @@
+git-issue-5637.dfy(1,0): Warning: File contains no code
+  |
+1 | // RUN: %translate cs --include-test-runner --allow-warnings %s > "%t"
+  | ^
+
+
+Dafny program verifier finished with 0 verified, 0 errors

docs/dev/news/5638.fix

@@ -0,0 +1 @@
+Crash when compiling an empty source file while including testing code