Added integration test + Reverted unit testing

Source/DafnyCore/Options/DeveloperOptionBag.cs

@@ -21,7 +21,7 @@ Print passified Boogie program translated from Dafny
     IsHidden = true,
     ArgumentHelpName = "file",
   };
-  // This flag is the only one that can trigger /dafnyVerify in the new CLI and I think it's sufficient
+
   public static readonly Option<string> BoogiePrint = new("--bprint",
   @"
 Print Boogie program translated from Dafny

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -22,6 +22,7 @@
 using JetBrains.Annotations;
 using Microsoft.Dafny;
 using Microsoft.Dafny.Triggers;
+using Serilog.Events;
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
@@ -700,6 +701,10 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) {
         return new Bpl.Program();
       }
 
+      if (Options.Get(CommonOptionBag.LogLevelOption).CompareTo(LogEventLevel.Verbose) <= 0) {
+        Options.OutputWriter.WriteLine("Starting translation to Boogie of module " + forModule.FullDafnyName);
+      }
+
       foreach (var plugin in p.Options.Plugins) {
         foreach (var rewriter in plugin.GetRewriters(p.Reporter)) {
           rewriter.PreVerify(forModule);

Source/DafnyDriver/Commands/RunCommand.cs

@@ -49,7 +49,7 @@ static RunCommand() {
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);
 
-  public static Command Create(Func<DafnyOptions, int> continuation = null) {
+  public static Command Create() {
     var result = new Command("run", "Run the program.");
     result.AddArgument(DafnyCommands.FileArgument);
     result.AddArgument(UserProgramArguments);
@@ -63,9 +63,7 @@ public static Command Create(Func<DafnyOptions, int> continuation = null) {
       options.Compile = true;
       options.RunAfterCompile = true;
       options.ForceCompile = options.Get(BoogieOptionBag.NoVerify);
-      if (continuation != null) {
-        return continuation(options);
-      }
+
       return await SynchronousCliCompilation.Run(options);
     });
     return result;

Source/DafnyDriver/DafnyNewCli.cs

@@ -172,10 +172,6 @@ private static void ProcessOption(InvocationContext context, Option option, Dafn
   }
 
   public static Task<int> Execute(IConsole console, IReadOnlyList<string> arguments) {
-    return ExecuteForParser(console, arguments, Parser);
-  }
-
-  public static Task<int> ExecuteForParser(IConsole console, IReadOnlyList<string> arguments, System.CommandLine.Parsing.Parser parser) {
     foreach (var symbol in AllSymbols) {
       if (symbol is Option option) {
         if (!option.Arity.Equals(ArgumentArity.ZeroOrMore) && !option.Arity.Equals(ArgumentArity.OneOrMore)) {
@@ -184,7 +180,7 @@ public static Task<int> ExecuteForParser(IConsole console, IReadOnlyList<string>
       }
     }
 
-    return parser.InvokeAsync(arguments.ToArray(), console);
+    return Parser.InvokeAsync(arguments.ToArray(), console);
   }
 
   private static readonly MethodInfo GetValueForOptionMethod;

Source/DafnyDriver/WritersConsole.cs

@@ -5,7 +5,7 @@
 
 namespace Microsoft.Dafny;
 
-public class WritersConsole : IConsole {
+class WritersConsole : IConsole {
   public TextReader InputWriter { get; }
   public TextWriter ErrWriter { get; }
   public TextWriter OutWriter { get; }

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCases.dfy

@@ -0,0 +1,25 @@
+// RUN: %baredafny run  %args --log-level verbose "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesNoTranslation.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify --bprint:file.bpl "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify --sprint:file.bpl "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify --sprint:file.bpl "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+module VerifiableModule {
+  @Test
+  method CanTest() {
+    assert 1 == 1;
+    expect 1 == 1;
+  }
+  method Main() {
+    CanTest();
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesNoTranslation.check

@@ -0,0 +1 @@
+// CHECK-NOT: Starting translation to Boogie of module VerifiableModule

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesTranslate.check

@@ -0,0 +1 @@
+// CHECK: Starting translation to Boogie of module VerifiableModule