Bring back --warn-as-errors for backwards compatibility (#5242)

### Description
Bring back --warn-as-errors for backwards compatibility

### How has this been tested?
Updated a littish test

<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>

CONTRIBUTING.md

@@ -101,3 +101,9 @@ For example, `Formatting.dfy`
 ### What is the release process?
 
 You can find a description of the release process in [docs/dev/RELEASE.md](https://github.com/dafny-lang/dafny/blob/master/docs/dev/RELEASE.md).
+
+### Backwards compatibility
+
+Dafny is still changing and backwards incompatible changes may be made. Any backwards compatibility breaking change must be easy to adapt to, such as by adding a command line option. In the future, we plan to add a `dafny migrate` command which should support migrating any Dafny codebase from the previous to the current CLI version. 
+
+As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -252,6 +252,10 @@ public enum GeneralTraitsOptions {
  @"In case the Dafny source code is translated to another language, emit that translation.") {
  };
 
+ public static readonly Option<bool> WarnAsErrors = new("--warn-as-errors", () => true, "(Deprecated). Please use --allow-warnings instead") {
+ IsHidden = true
+ };
+
  public static readonly Option<bool> AllowWarnings = new("--allow-warnings",
  "Allow compilation to continue and succeed when warnings occur. Errors will still halt and fail compilation.");
 
@@ -355,6 +359,14 @@ public enum DefaultFunctionOpacityOptions {
  };
 
  static CommonOptionBag() {
+ DafnyOptions.RegisterLegacyBinding(WarnAsErrors, (options, value) => {
+ if (!options.Get(AllowWarnings) && !options.Get(WarnAsErrors)) {
+ // If allow warnings is at the default value, and warn-as-errors is not, use the warn-as-errors value
+ options.Set(AllowWarnings, true);
+ options.FailOnWarnings = false;
+ }
+ });
+
  DafnyOptions.RegisterLegacyUi(AllowAxioms, DafnyOptions.ParseBoolean, "Verification options", legacyName: "allowAxioms", defaultValue: true);
  DafnyOptions.RegisterLegacyBinding(ShowInference, (options, value) => {
  options.PrintTooltips = value;
@@ -577,6 +589,7 @@ public enum DefaultFunctionOpacityOptions {
  }
  );
  DooFile.RegisterNoChecksNeeded(
+ WarnAsErrors,
  ProgressOption,
  LogLocation,
  LogLevelOption,

Source/DafnyCore/Options/DafnyCommands.cs

@@ -76,6 +76,7 @@ public static class DafnyCommands {
  DeveloperOptionBag.BoogiePrint,
  Printer.PrintMode,
  CommonOptionBag.AllowWarnings,
+ CommonOptionBag.WarnAsErrors
  });
 
  public static readonly IReadOnlyList<Option> ParserOptions = new List<Option>(new Option[] {

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/pass-on-warnings.dfy → Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/allow-warnings.dfy

@@ -1,4 +1,5 @@
 // RUN: %build --warn-shadowing --allow-warnings "%s" > "%t"
+// RUN: %build --warn-shadowing --warn-as-errors=false "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 method f(x: int) {
  var x := 0;

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/allow-warnings.dfy.expect

@@ -0,0 +1,6 @@
+allow-warnings.dfy(5,6): Warning: Shadowed local-variable name: x
+
+Dafny program verifier finished with 0 verified, 0 errors
+allow-warnings.dfy(5,6): Warning: Shadowed local-variable name: x
+
+Dafny program verifier finished with 0 verified, 0 errors