Allow the :test attribute when using run and build (dafny-lang#3275)

Fixes dafny-lang#3260

Also adds a hidden `--spill-translation` attribute for the `run`,`build`
and `test` commands.

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

Source/DafnyCore/Compilers/Compiler-Csharp.cs

@@ -3390,7 +3390,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
  }
 
  private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSyntaxTree wr) {
- if (DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) {
+ if (DafnyOptions.O.Compile || DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) {
  return;
  }
 

Source/DafnyCore/Options/DeveloperOptionBag.cs

@@ -5,13 +5,18 @@ namespace Microsoft.Dafny;
 
 public class DeveloperOptionBag {
 
+ public static readonly Option<bool> SpillTranslation = new("--spill-translation",
+ @"In case the Dafny source code is translated to another language, emit that translation.") {
+ IsHidden = true
+ };
+
  public static readonly Option<bool> UseBaseFileName = new("--use-basename-for-filename",
  "When parsing use basename of file for tokens instead of the path supplied on the command line") {
  IsHidden = true
  };
 
  public static readonly Option<string> BoogiePrint = new("--bprint",
-  @"
+ @"
 Print Boogie program translated from Dafny
 (use - as <file> to print to console)".TrimStart()) {
  IsHidden = true,
@@ -33,6 +38,8 @@ Print Dafny program after resolving it.
  };
 
  static DeveloperOptionBag() {
+ DafnyOptions.RegisterLegacyBinding(SpillTranslation, (o, f) => o.SpillTargetCode = f ? 1U : 0U);
+
  DafnyOptions.RegisterLegacyBinding(ResolvedPrint, (options, value) => {
  options.DafnyPrintResolvedFile = value;
  options.ExpandFilename(options.DafnyPrintResolvedFile, x => options.DafnyPrintResolvedFile = x, options.LogPrefix,

Source/DafnyCore/Options/ICommandSpec.cs

@@ -34,7 +34,8 @@ static ICommandSpec() {
  }.Concat(VerificationOptions).ToList();
 
  public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
- CommonOptionBag.Target
+ CommonOptionBag.Target,
+ DeveloperOptionBag.SpillTranslation
  }.Concat(TranslationOptions).ToList();
 
  public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {

docs/check-examples

@@ -36,20 +36,20 @@
 ## %no-check : do nothing
 ## %check-verify <expect> or
 ## %check-verify-warn : runs the command 
-## "dafny verify --useBaseNameForFileName $F" and checks 
+## "dafny verify --use-basename-for-filename $F" and checks
 ## (1) if <expect> is absent then the exit code is 0 and
 ## the output is just a success message
 ## (2) if <expect> is non-empty. then the exit code is 4 and
 ## the actual output matches the content of the file <expect>
 ## if the command is %check-verify-warn, the exit code is 0
 ## %check-resolve <expect> : runs the command
-## "dafny resolve --useBaseNameForFileName $F" and checks
+## "dafny resolve --use-basename-for-filename $F" and checks
 ## (1) if <expect> is absent then the exit code is 0 and
 ## the output is just a success message
 ## (2) if <expect> is non-empty. then the exit code is 2 and
 ## the actual output matches the content of the file <expect>
 ## %check-run <expect> : runs the command
-## "dafny run --useBaseNameForFileName $F" and, 
+## "dafny run --use-basename-for-filename $F" and,
 ## if <expect> is present, then the output matches the
 ## content of the file names <expect>
 ## %check-error