Fix: Other CLI files that are not found do not trigger exceptions (da…

…fny-lang#3331)

Source/DafnyCore/DafnyMain.cs

@@ -78,6 +78,9 @@ public DafnyFile(string filePath, bool useStdin = false) {
  }
 
  private static string GetDafnySourceAttributeText(string dllPath) {
+ if (!File.Exists(dllPath)) {
+ throw new IllegalDafnyFile();
+ }
  using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite);
  using var dllPeReader = new PEReader(dllFs);
  var dllMetadataReader = dllPeReader.GetMetadataReader();

Source/DafnyDriver/DafnyDriver.cs

@@ -259,7 +259,13 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar
 
  var supportedExtensions = options.Compiler.SupportedExtensions;
  if (supportedExtensions.Contains(extension)) {
- otherFiles.Add(file);
+ // .h files are not part of the build, they are just emitted as includes
+ if (File.Exists(file) || extension == ".h") {
+ otherFiles.Add(file);
+ } else {
+ options.Printer.ErrorWriteLine(Console.Out, $"*** Error: file {file} not found");
+ return CommandLineArgumentsResult.PREPROCESSING_ERROR;
+ }
  } else if (!isDafnyFile) {
  if (string.IsNullOrEmpty(extension) && file.Length > 0 && (file[0] == '/' || file[0] == '-')) {
  options.Printer.ErrorWriteLine(Console.Out,

Test/git-issues/git-issue-2719.dfy

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

Test/git-issues/git-issue-2719.dfy.expect

@@ -0,0 +1 @@
+*** Error: file foobar.dll not found

Test/git-issues/git-issue-590.dfy.expect

@@ -1 +1 @@
-*** Error: The command-line contains no .dfy files
+*** Error: file x.cs not found

docs/dev/news/2719.fix

@@ -0,0 +1 @@
+Nonexistent files passed on the CLI result in a graceful exit