Merge branch 'master' into SelfReference

Source/DafnyCore/DafnyFile.cs

@@ -31,6 +31,7 @@ public class DafnyFile {
  CanonicalPath = contentOverride == null ? Canonicalize(filePath).LocalPath : "<stdin>";
  filePath = CanonicalPath;
 
+ var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath;
  if (contentOverride != null) {
  IsPreverified = false;
  IsPrecompiled = false;
@@ -46,7 +47,7 @@ public class DafnyFile {
  return;
  }
 
- options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePath} not found");
+ options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
  throw new IllegalDafnyFile(true);
  } else {
  Content = new StreamReader(filePath);
@@ -55,9 +56,11 @@ public class DafnyFile {
  IsPreverified = true;
  IsPrecompiled = false;
 
+ if (!File.Exists(filePath)) {
+ options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
+ throw new IllegalDafnyFile(true);
+ }
  var dooFile = DooFile.Read(filePath);
-
- var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath;
  if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) {
  throw new IllegalDafnyFile(true);
  }

Source/DafnyDriver/Commands/CommandRegistry.cs

@@ -244,14 +244,17 @@ class WritersConsole : IConsole {
  }
 
  private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) {
+ var filePathForErrors = dafnyOptions.UseBaseNameForFileName
+ ? Path.GetFileName(singleFile.FullName)
+ : singleFile.FullName;
  if (Path.GetExtension(singleFile.FullName) == ".toml") {
  if (dafnyOptions.ProjectFile != null) {
- dafnyOptions.ErrorWriter.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {singleFile.FullName} were specified");
+ dafnyOptions.ErrorWriter.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {filePathForErrors} were specified");
  return false;
  }
 
  if (!File.Exists(singleFile.FullName)) {
- dafnyOptions.ErrorWriter.WriteLine($"Error: file {singleFile.FullName} not found");
+ dafnyOptions.ErrorWriter.WriteLine($"Error: file {filePathForErrors} not found");
  return false;
  }
  var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), dafnyOptions.ErrorWriter);

Source/DafnyDriver/DafnyDriver.cs

@@ -272,6 +272,10 @@ public enum CommandLineArgumentsResult {
  if (extension != null) { extension = extension.ToLower(); }
 
  bool isDafnyFile = false;
+ var relative = System.IO.Path.GetFileName(file);
+ bool useRelative = options.UseBaseNameForFileName || relative.StartsWith("-");
+ var nameToShow = useRelative ? relative
+ : Path.GetRelativePath(Directory.GetCurrentDirectory(), file);
  try {
  var df = new DafnyFile(options, Path.GetFullPath(file));
  if (options.LibraryFiles.Contains(file)) {
@@ -283,17 +287,19 @@ public enum CommandLineArgumentsResult {
  }
  dafnyFiles.Add(df);
  isDafnyFile = true;
+ } catch (ArgumentException e) {
+ options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: {0}: ", nameToShow, e.Message);
+ return CommandLineArgumentsResult.PREPROCESSING_ERROR;
  } catch (IllegalDafnyFile e) {
  if (e.ProcessingError) {
  return CommandLineArgumentsResult.PREPROCESSING_ERROR;
  }
  // Fall through and try to handle the file as an "other file"
+ } catch (Exception e) {
+ options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: {0}: {1}", nameToShow, e.Message);
+ return CommandLineArgumentsResult.PREPROCESSING_ERROR;
  }
 
- var relative = System.IO.Path.GetFileName(file);
- bool useRelative = options.UseBaseNameForFileName || relative.StartsWith("-");
- var nameToShow = useRelative ? relative
- : Path.GetRelativePath(Directory.GetCurrentDirectory(), file);
  var supportedExtensions = options.Backend.SupportedExtensions;
  if (supportedExtensions.Contains(extension)) {
  // .h files are not part of the build, they are just emitted as includes

Test/dafny0/formatting2.dfy.expect

@@ -1 +1 @@
-*** Error: file /unexisting.dfy not found
+*** Error: file unexisting.dfy not found

Test/doofiles/BadDoo.doo

@@ -0,0 +1,2 @@
+
+Doo file with incorrect content

Test/doofiles/Test1.dfy

@@ -0,0 +1,6 @@
+// RUN: %exits-with 1 %baredafny resolve --use-basename-for-filename "%s" "%S/NoSuch.doo" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Input .doo file does not exist
+
+const c := 42

Test/doofiles/Test1.dfy.expect

@@ -0,0 +1 @@
+*** Error: file NoSuch.doo not found

Test/doofiles/Test2.dfy

@@ -0,0 +1,6 @@
+// RUN: %exits-with 1 %baredafny resolve --use-basename-for-filename "%s" "%S/BadDoo.doo" 2> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Input .doo file has invalid content
+
+const c := 42

Test/doofiles/Test2.dfy.expect

@@ -0,0 +1 @@
+*** Error: BadDoo.doo: End of Central Directory record could not be found.

Test/doofiles/Test3.dfy

@@ -0,0 +1,7 @@
+// RUN: %baredafny build -t:lib --use-basename-for-filename "%s" --output "%S/test" > "%t"
+// RUN: %baredafny resolve --use-basename-for-filename "%S/Test3a.dfy" "%S/test.doo" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Output file does not have a .doo suffix; test.doo created
+
+const c := 42

Test/doofiles/Test3.dfy.expect

@@ -0,0 +1,4 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+
+Dafny program verifier did not attempt verification

Test/doofiles/Test3a.dfy

@@ -0,0 +1,6 @@
+// RUN: %baredafny --help
+
+
+// Just an auxiliary file to Test3.dfy
+
+const d := 42

Test/doofiles/Test4.dfy

@@ -0,0 +1,8 @@
+// RUN: %baredafny build -t:lib --use-basename-for-filename "%s" --output "%S/test2" > "%t"
+// RUN: %baredafny resolve --use-basename-for-filename "%s" "%S/test2.doo" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+// XFAIL: *
+
+// Combining a file with a .doo of itself -- was a crash
+
+const c := 42

Test/doofiles/Test5.dfy

@@ -0,0 +1,6 @@
+// RUN: %exits-with 1 %baredafny build -t:lib --use-basename-for-filename "%s" --output: 2> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Missing output
+
+const c := 42

Test/doofiles/Test5.dfy.expect

@@ -0,0 +1,2 @@
+Required argument missing for option: '--output'.
+

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

@@ -0,0 +1,7 @@
+// RUN: %exits-with 1 %baredafny build -t:lib --use-basename-for-filename "%s" x.doo > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Tests case in which an input .doo file does not exist
+const c := 5
+
+

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

@@ -0,0 +1 @@
+*** Error: file x.doo not found

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

@@ -1,4 +1,4 @@
 // dafny should emit exit value 1
-// RUN: ! %dafny /xyz   > "%t"
+// RUN: ! %dafny /xyz /useBasenameForFilename > "%t"
 // RUN: %diff "%s.expect" "%t"
 // UNSUPPORTED: windows

docs/DafnyRef/UserGuide.md

@@ -108,7 +108,7 @@ identified with the name `lib` on the command line. For example, to build multip
 Dafny files into a single build artifact for shared reuse, the command would look something like:
 
 ```bash
-dafny build -t:lib A.dfy B.dfy C.dfy --out MyLib.doo
+dafny build -t:lib A.dfy B.dfy C.dfy --output:MyLib.doo
 ```
 
 The Dafny code contained in a `.doo` file is not re-verified when passed back to the `dafny` tool,

docs/Gemfile

@@ -12,7 +12,7 @@ source "https://rubygems.org"
 gem "minima", "~> 2.5"
 # If you want to use GitHub Pages, remove the "gem "jekyll"" above and
 # uncomment the line below. To upgrade, run `bundle update github-pages`.
-gem "github-pages", "~> 225", group: :jekyll_plugins
+gem "github-pages", "~> 228", group: :jekyll_plugins
 # If you have any plugins, put them here!
 #group :jekyll_plugins do
 # gem "jekyll-feed", "~> 0.12"
@@ -24,7 +24,7 @@ gem "kramdown", ">= 2.3.1"
 # Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem
 # and associated library.
 platforms :mingw, :x64_mingw, :mswin, :jruby do
- gem "tzinfo", "~> 1.2"
+ gem "tzinfo", "~> 2.0"
  gem "tzinfo-data"
 end
 

docs/Gemfile.lock

@@ -1,45 +1,45 @@
 GEM
  remote: https://rubygems.org/
  specs:
- activesupport (6.0.6.1)
+ activesupport (6.1.7.3)
  concurrent-ruby (~> 1.0, >= 1.0.2)
- i18n (>= 0.7, < 2)
- minitest (~> 5.1)
- tzinfo (~> 1.1)
- zeitwerk (~> 2.2, >= 2.2.2)
- addressable (2.8.0)
- public_suffix (>= 2.0.2, < 5.0)
+ i18n (>= 1.6, < 2)
+ minitest (>= 5.1)
+ tzinfo (~> 2.0)
+ zeitwerk (~> 2.3)
+ addressable (2.8.4)
+ public_suffix (>= 2.0.2, < 6.0)
  coffee-script (2.4.1)
  coffee-script-source
  execjs
  coffee-script-source (1.11.1)
  colorator (1.1.0)
  commonmarker (0.23.9)
- concurrent-ruby (1.2.0)
- dnsruby (1.61.9)
- simpleidn (~> 0.1)
+ concurrent-ruby (1.2.2)
+ dnsruby (1.70.0)
+ simpleidn (~> 0.2.1)
  em-websocket (0.5.3)
  eventmachine (>= 0.12.9)
  http_parser.rb (~> 0)
- ethon (0.15.0)
+ ethon (0.16.0)
  ffi (>= 1.15.0)
  eventmachine (1.2.7)
  execjs (2.8.1)
- faraday (2.3.0)
- faraday-net_http (~> 2.0)
+ faraday (2.7.5)
+ faraday-net_http (>= 2.0, < 3.1)
  ruby2_keywords (>= 0.0.4)
- faraday-net_http (2.0.3)
+ faraday-net_http (3.0.2)
  ffi (1.15.5)
  ffi (1.15.5-x64-mingw-ucrt)
  ffi (1.15.5-x64-unknown)
  forwardable-extended (2.6.0)
  gemoji (3.0.1)
- github-pages (225)
+ github-pages (228)
  github-pages-health-check (= 1.17.9)
- jekyll (= 3.9.0)
+ jekyll (= 3.9.3)
  jekyll-avatar (= 0.7.0)
  jekyll-coffeescript (= 1.1.1)
- jekyll-commonmark-ghpages (= 0.2.0)
+ jekyll-commonmark-ghpages (= 0.4.0)
  jekyll-default-layout (= 0.1.4)
  jekyll-feed (= 0.15.1)
  jekyll-gist (= 1.5.0)
@@ -71,12 +71,12 @@ GEM
  jekyll-theme-time-machine (= 0.2.0)
  jekyll-titles-from-headings (= 0.5.3)
  jemoji (= 0.12.0)
- kramdown (= 2.3.1)
+ kramdown (= 2.3.2)
  kramdown-parser-gfm (= 1.1.0)
- liquid (= 4.0.3)
+ liquid (= 4.0.4)
  mercenary (~> 0.3)
  minima (= 2.5.1)
- nokogiri (>= 1.12.5, < 2.0)
+ nokogiri (>= 1.13.6, < 2.0)
  rouge (= 3.26.0)
  terminal-table (~> 1.4)
  github-pages-health-check (1.17.9)
@@ -85,17 +85,17 @@ GEM
  octokit (~> 4.0)
  public_suffix (>= 3.0, < 5.0)
  typhoeus (~> 1.3)
- html-pipeline (2.14.1)
+ html-pipeline (2.14.3)
  activesupport (>= 2)
  nokogiri (>= 1.4)
  http_parser.rb (0.8.0)
- i18n (0.9.5)
+ i18n (1.13.0)
  concurrent-ruby (~> 1.0)
- jekyll (3.9.0)
+ jekyll (3.9.3)
  addressable (~> 2.4)
  colorator (~> 1.0)
  em-websocket (~> 0.5)
- i18n (~> 0.7)
+ i18n (>= 0.7, < 2)
  jekyll-sass-converter (~> 1.0)
  jekyll-watch (~> 2.0)
  kramdown (>= 1.17, < 3)
@@ -111,11 +111,11 @@ GEM
  coffee-script-source (~> 1.11.1)
  jekyll-commonmark (1.4.0)
  commonmarker (~> 0.22)
- jekyll-commonmark-ghpages (0.2.0)
- commonmarker (~> 0.23.4)
+ jekyll-commonmark-ghpages (0.4.0)
+ commonmarker (~> 0.23.7)
  jekyll (~> 3.9.0)
  jekyll-commonmark (~> 1.4.0)
- rouge (>= 2.0, < 4.0)
+ rouge (>= 2.0, < 5.0)
  jekyll-default-layout (0.1.4)
  jekyll (~> 3.0)
  jekyll-feed (0.15.1)
@@ -200,36 +200,37 @@ GEM
  gemoji (~> 3.0)
  html-pipeline (~> 2.2)
  jekyll (>= 3.0, < 5.0)
- kramdown (2.3.1)
+ kramdown (2.3.2)
  rexml
  kramdown-parser-gfm (1.1.0)
  kramdown (~> 2.0)
- liquid (4.0.3)
- listen (3.7.1)
+ liquid (4.0.4)
+ listen (3.8.0)
  rb-fsevent (~> 0.10, >= 0.10.3)
  rb-inotify (~> 0.9, >= 0.9.10)
  mercenary (0.3.6)
- mini_portile2 (2.8.1)
+ mini_portile2 (2.8.2)
  minima (2.5.1)
  jekyll (>= 3.5, < 5.0)
  jekyll-feed (~> 0.9)
  jekyll-seo-tag (~> 2.1)
- minitest (5.17.0)
- nokogiri (1.14.3)
- mini_portile2 (~> 2.8.0)
+ minitest (5.18.0)
+ nokogiri (1.15.2)
+ mini_portile2 (~> 2.8.2)
+ racc (~> 1.4)
  racc (~> 1.4)
  nokogiri (1.14.3-x64-mingw-ucrt)
  racc (~> 1.4)
  nokogiri (1.14.3-x86_64-linux)
  racc (~> 1.4)
- octokit (4.25.0)
+ octokit (4.25.1)
  faraday (>= 1, < 3)
  sawyer (~> 0.9)
  pathutil (0.16.2)
  forwardable-extended (~> 2.6)
  public_suffix (4.0.7)
  racc (1.6.2)
- rb-fsevent (0.11.1)
+ rb-fsevent (0.11.2)
  rb-inotify (0.10.1)
  ffi (~> 1.0)
  rexml (3.2.5)
@@ -249,11 +250,10 @@ GEM
  unf (~> 0.1.4)
  terminal-table (1.8.0)
  unicode-display_width (~> 1.1, >= 1.1.1)
- thread_safe (0.3.6)
  typhoeus (1.4.0)
  ethon (>= 0.9.0)
- tzinfo (1.2.10)
- thread_safe (~> 0.1)
+ tzinfo (2.0.6)
+ concurrent-ruby (~> 1.0)
  tzinfo-data (1.2023.3)
  tzinfo (>= 1.0.0)
  unf (0.1.4)
@@ -263,21 +263,21 @@ GEM
  unf_ext (0.0.8.2-x64-unknown)
  unicode-display_width (1.8.0)
  wdm (0.1.1)
- zeitwerk (2.6.6)
+ zeitwerk (2.6.8)
 
 PLATFORMS
  x64-mingw-ucrt
  x64-unknown
  x86_64-linux
 
 DEPENDENCIES
- github-pages (~> 225)
+ github-pages (~> 228)
  jekyll-numbered-headings
  kramdown (>= 2.3.1)
  minima (~> 2.5)
- tzinfo (~> 1.2)
+ tzinfo (~> 2.0)
  tzinfo-data
  wdm (~> 0.1.1)
 
 BUNDLED WITH
- 2.3.8
+ 2.4.13