Add deprecation warning for old CLI (#5249)

### Description - Add deprecation warning for old CLI ### How has this been tested? - Updated CLI tests <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>
dafny-lang · Apr 10, 2024 · d8b081e · d8b081e
1 parent 281ed82
commit d8b081e
Show file tree

Hide file tree

Showing 43 changed files with 94 additions and 49 deletions.
diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier did not attempt verification
 Wrote textual form of target program to GroceryListPrinter.cs

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
@@ -480,7 +480,7 @@ public enum IncludesModes {
  return base.ParseOption(name, ps);
  }
 
- public override string Help => "Use 'dafny --help' to see help for a newer Dafny CLI format.\n" +
+ public override string Help => "Use 'dafny --help' to see help for the new Dafny CLI format.\n" +
  LegacyUiForOption.GenerateHelp(base.Help, LegacyUis, true);
 
  protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState ps) {

diff --git a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs
@@ -88,6 +88,11 @@ public static class DafnyBackwardsCompatibleCli {
  return new ExitImmediately(ExitValue.SUCCESS);
  }
 
+ if (oldOptions.DeprecationNoise != 0) {
+ oldOptions.OutputWriter.WriteLine(
+ "Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format");
+ }
+
  return new ParsedOptions(oldOptions);
  }
 

diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -144,8 +144,8 @@ public class SynchronousCliCompilation : IDisposable {
  dafnyFiles.Add(df);
  isDafnyFile = true;
  }
- } catch (ArgumentException e) {
- options.ErrorWriter.WriteLine("*** Error: {0}: ", nameToShow, e.Message);
+ } catch (ArgumentException) {
+ options.ErrorWriter.WriteLine("*** Error: {0}: ", nameToShow);
  return ExitValue.PREPROCESSING_ERROR;
  } catch (Exception e) {
  options.ErrorWriter.WriteLine("*** Error: {0}: {1}", nameToShow, e.Message);

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect
@@ -9,12 +9,14 @@ Dafny program verifier finished with 1 verified, 2 errors
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":16}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}
 
 Dafny program verifier finished with 1 verified, 2 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":15,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":14,"character":8}}},"severity":4,"message":"newtype byte resolves as target-complete {:nativeType \u0022byte\u0022} (detected range: 0 .. 256)","source":"Resolver","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":16,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":16}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}
 
 Dafny program verifier finished with 1 verified, 2 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":15,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":16,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":14},"end":{"line":19,"character":18}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:https:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35},"end":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}

diff --git a/...onTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy.expect b/...onTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 42 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BranchCoverage.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -84,6 +85,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -170,6 +172,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -256,6 +259,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled
@@ -342,6 +346,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 39: 10
 40: 1
 41: 3
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 6 verified, 0 errors
 0: BranchCoverage.dfy(20,21): entry to method _module._default.NeverCalled

diff --git a/...grationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
 CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DafnyLibClient.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DafnyLibClient.dfy.expect
@@ -1,5 +1,7 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 3 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 1 verified, 0 errors
 hello from the library

diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
 bye
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Superposition.legacy.dfy(38,9): Warning: the ... refinement feature in statements is deprecated
 
 Verifying M0.C.M (correctness) ...

diff --git a/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots3.run.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots3.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots3.v0.dfy(9,14)) assert {:id "id0"} Lit(0 != 0);
  >>> DoNothingToAssert
 Snapshots3.v0.dfy(9,13): Error: assertion might not hold

diff --git a/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots4.run.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots4.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots4.v0.dfy(9,14)) assert {:id "id0"} LitInt(0) == LitInt(0);
  >>> DoNothingToAssert
 

diff --git a/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots8.v0.dfy(2,37)) assert {:id "id0"} x#0 < 20 || LitInt(10) <= x#0;
  >>> DoNothingToAssert
 Processing command (at Snapshots8.v0.dfy(3,12)) assert {:id "id1"} x#0 < 10;

diff --git a/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect b/...grationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0;
  >>> DoNothingToAssert
 Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/InductionOptions.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/InductionOptions.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 InductionOptions.legacy.dfy(21,0): Error: a postcondition could not be proved on this return path
 InductionOptions.legacy.dfy(20,26): Related location: this is the postcondition that could not be proved
 InductionOptions.legacy.dfy(25,9): Error: assertion might not hold
@@ -17,12 +18,15 @@ InductionOptions.legacy.dfy(29,10): Related location: this is the postcondition
 InductionOptions.legacy.dfy(35,9): Error: assertion might not hold
 
 Dafny program verifier finished with 3 verified, 4 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 InductionOptions.legacy.dfy(21,0): Error: a postcondition could not be proved on this return path
 InductionOptions.legacy.dfy(20,26): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 6 verified, 1 error
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 7 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 InductionOptions.legacy.dfy(25,9): Error: assertion might not hold
 InductionOptions.legacy.dfy(30,0): Error: a postcondition could not be proved on this return path
 InductionOptions.legacy.dfy(29,10): Related location: this is the postcondition that could not be proved

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug128.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug128.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-down.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-down.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 12 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy.expect
@@ -1,2 +1,3 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue158.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue158.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 4 verified, 0 errors
 map[Record.Make(null, null, _module.Class, 5, 10) := 0.8]
@@ -24,6 +25,7 @@ false
 false false
 false false
 true true
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 4 verified, 0 errors
 map[Record.Make(null, null, _module.Class, 5, 10) := 0.8]

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue250.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue250.dfy.expect
@@ -1,20 +1,30 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Verifying foo (correctness) ...
  [1 proof obligation] error

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy.expect
@@ -4,6 +4,7 @@ git-issue-1248.dfy(19,0): Error: a postcondition could not be proved on this ret
 git-issue-1248.dfy(18,10): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 2 errors
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-1248.dfy(13,0): Error: a postcondition could not be proved on this return path
 git-issue-1248.dfy(12,10): Related location: this is the postcondition that could not be proved
 git-issue-1248.dfy(19,0): Error: a postcondition could not be proved on this return path

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-19c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-19c.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-19c.dfy(41,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'basic' (of type 'Basic') may contain references (see documentation for 'older' parameters)
 git-issue-19c.dfy(86,12): Error: a set comprehension involved in a function definition (implicitly by using a function in a reads clause) is not allowed to depend on the set of allocated references, but values of '_x0' (of type 'Basic') may contain references (see documentation for 'older' parameters)
 git-issue-19c.dfy(93,12): Error: a set comprehension involved in a function definition (implicitly by using a function in a reads clause) is not allowed to depend on the set of allocated references, but values of '_x0' (of type 'X') may contain references (perhaps declare its type as 'X(!new)') (see documentation for 'older' parameters)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy
@@ -20,5 +20,5 @@ method Main() {
  print "2 in seq? ", f(2),"\n";
  var g := InSeq2([1, 2]);
  print "2 in seq? ", g(2),"\n";
- print "All right";
+ print "All right", "\n";
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2690.dfy.expect
@@ -1,9 +1,12 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 3 verified, 0 errors
 2 in seq? true
 2 in seq? true
 All right
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
+
 Dafny program verifier did not attempt verification
 2 in seq? true
 2 in seq? true
-All right
+All right
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2719.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2719.dfy.expect
@@ -1 +1,2 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: file foobar.dll not found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-277.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-277.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-277.dfy(5,12): Error: wrong number of indices for multi-selection
 git-issue-277.dfy(5,25): Error: wrong number of indices for multi-selection
 git-issue-277.dfy(5,12): Error: incorrect type for selection into array<int> (got bool)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2843.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2843.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 git-issue-2843.dfy(14,7): Error: a function with ghost parameters can be used as a value only in specification contexts
 git-issue-2843.dfy(20,7): Error: a ghost function is allowed only in specification contexts
 git-issue-2843.dfy(33,8): Error: ghost variables such as f are allowed only in specification contexts. f was inferred to be ghost based on its declaration or initialization.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3267.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3267.dfy.expect
@@ -1,7 +1,10 @@
 *** Error: 'zzzz': The first input must be a command or a legacy option or file with supported extension
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: 'test.d': Filename extension '.d' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files (.cs, .dll)
 CLI: Error: command-line argument '--zzzz' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
 CLI: Error: command-line argument 'test' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
 CLI: Error: command-line argument 'test.d' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: 'test.d': Filename extension '.d' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files (.cs, .dll)
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: Command-line argument 'zzzz' is neither a recognized option nor a filename with a supported extension (.dfy, .cs, .dll).
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-645.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-645.dfy.expect
@@ -1 +1,2 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 *** Error: Command-line argument 'xyz' is neither a recognized option nor a filename with a supported extension (.dfy, .cs, .dll).
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 21 verified, 0 errors
 xs = List.Cons(57, List.Cons(100, List.Cons(-34, List.Cons(1, List.Cons(8, List.Nil)))))

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs0.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 inheritreqs0.dfy(19,13): Error: a precondition for this call could not be proved
 inheritreqs0.dfy[Impl](6,17): Related location: this is the precondition that could not be proved
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/inheritreqs1.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 inheritreqs1.dfy(20,13): Error: a precondition for this call could not be proved
 inheritreqs1.dfy(15,17): Related location: this is the precondition that could not be proved
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/optimize0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/optimize0.dfy.expect
@@ -1,3 +1,4 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
 
 Dafny program verifier finished with 0 verified, 0 errors
 o hai!