diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 1ba0a18d7b5..ced6f1caedc 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/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(); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 1a32b7bd73e..775bbccd3cb 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/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, diff --git a/Test/git-issues/git-issue-2719.dfy b/Test/git-issues/git-issue-2719.dfy new file mode 100644 index 00000000000..672b7cb90cf --- /dev/null +++ b/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" diff --git a/Test/git-issues/git-issue-2719.dfy.expect b/Test/git-issues/git-issue-2719.dfy.expect new file mode 100644 index 00000000000..1f8b85a60e4 --- /dev/null +++ b/Test/git-issues/git-issue-2719.dfy.expect @@ -0,0 +1 @@ +*** Error: file foobar.dll not found diff --git a/Test/git-issues/git-issue-590.dfy.expect b/Test/git-issues/git-issue-590.dfy.expect index b552c99f434..6cb7056f22b 100644 --- a/Test/git-issues/git-issue-590.dfy.expect +++ b/Test/git-issues/git-issue-590.dfy.expect @@ -1 +1 @@ -*** Error: The command-line contains no .dfy files +*** Error: file x.cs not found diff --git a/docs/dev/news/2719.fix b/docs/dev/news/2719.fix new file mode 100644 index 00000000000..7b59a02c835 --- /dev/null +++ b/docs/dev/news/2719.fix @@ -0,0 +1 @@ +Nonexistent files passed on the CLI result in a graceful exit