Avoiding a crash on empty input filename - Issue #3549 (#3899)

Fixes #3549

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: davidcok <[email protected]>

Source/DafnyCore/DafnyOptions.cs

@@ -225,11 +225,16 @@ public override bool Parse(string[] arguments) {
         }
       }
 
-      if (i >= arguments.Length) {
-        return base.Parse(arguments);
+      try {
+        if (i >= arguments.Length) {
+          return base.Parse(arguments);
+        }
+        MainArgs = arguments.Skip(i + 1).ToList();
+        return base.Parse(arguments.Take(i).ToArray());
+      } catch (Exception e) {
+        ErrorWriter.WriteLine("Invalid filename: " + e.Message);
+        return false;
       }
-      MainArgs = arguments.Skip(i + 1).ToList();
-      return base.Parse(arguments.Take(i).ToArray());
     }
 
     public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter)

Source/XUnitExtensions/Lit/ILitCommand.cs

@@ -64,17 +64,20 @@ public static Token[] Tokenize(string line) {
       var singleQuoted = false;
       var doubleQuoted = false;
       var kind = Kind.Verbatim;
+      var tokenStarted = false;
       foreach (var c in line) {
         if (c == '\'' && !doubleQuoted) {
           singleQuoted = !singleQuoted;
+          tokenStarted = true;
         } else if (c == '"' && !singleQuoted) {
           doubleQuoted = !doubleQuoted;
+          tokenStarted = true;
         } else if (Char.IsWhiteSpace(c) && !(singleQuoted || doubleQuoted)) {
-          if (inProgressArgument.Length != 0) {
+          if (tokenStarted) {
             result.Add(new Token(inProgressArgument.ToString(), kind));
-
             inProgressArgument.Clear();
             kind = Kind.Verbatim;
+            tokenStarted = false;
           }
         } else {
           if (c is '?' && inProgressArgument.Length == 1 && inProgressArgument[0] == '-') {
@@ -83,10 +86,13 @@ public static Token[] Tokenize(string line) {
             kind = Kind.MustGlob;
           }
           inProgressArgument.Append(c);
+          tokenStarted = true;
         }
       }
 
-      result.Add(new Token(inProgressArgument.ToString(), kind));
+      if (tokenStarted) {
+        result.Add(new Token(inProgressArgument.ToString(), kind));
+      }
 
       return result.ToArray();
     }

Test/git-issues/git-issue-3549a.dfy

@@ -0,0 +1,2 @@
+// RUN: %exits-with 1 %baredafny "" 2> "%t"
+// RUN: %diff "%s.expect" "%t"

Test/git-issues/git-issue-3549a.dfy.expect

@@ -0,0 +1 @@
+Invalid filename: The path is empty. (Parameter 'path')

Test/git-issues/git-issue-3549b.dfy

@@ -0,0 +1,2 @@
+// RUN: %exits-with 1 %baredafny resolve "" 2> "%t"
+// RUN: %diff "%s.expect" "%t"

Test/git-issues/git-issue-3549b.dfy.expect

@@ -0,0 +1 @@
+*** Error: No input files were specified in command-line resolve|.

docs/dev/3549.fix

@@ -0,0 +1 @@
+Fixed crash on an empty filename