dafny-lang · atomb · Jun 7, 2023 · Jun 7, 2023
diff --git a/Source/DafnyCore/TestGenerationOptions.cs b/Source/DafnyCore/TestGenerationOptions.cs
@@ -12,7 +12,6 @@ public enum Modes { None, Block, Path };
     public Modes Mode = Modes.None;
     [CanBeNull] public string TargetMethod = null;
     public uint SeqLengthLimit = 0;
-    public bool Verbose = false;
     [CanBeNull] public string PrintBpl = null;
     [CanBeNull] public string PrintStats = null;
     public bool DisablePrune = false;
@@ -58,10 +57,6 @@ public bool ParseOption(string name, Bpl.CommandLineParseState ps) {
           }
           return true;
 
-        case "generateTestVerbose":
-          Verbose = true;
-          return true;
-
         case "generateTestNoPrune":
           DisablePrune = true;
           return true;
@@ -87,8 +82,6 @@ Add an axiom that sets the length of all sequences to be no greater
     If specified, only this method will be tested.
 /generateTestPrintBpl:<fileName>
     Print the Boogie code used during test generation.
-/generateTestVerbose
-    Print various debugging info as comments for the generated tests.
 /generateTestNoPrune
     Disable axiom pruning that Dafny uses to speed up verification.";
 

diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs
@@ -426,12 +426,12 @@ private void VisitUserDefinedTypeDeclaration(string newTypeName,
         Type baseType, Expression/*?*/ witness, List<TypeParameter> typeArgs) {
         if (witness != null) {
           info.witnessForType[newTypeName] = witness;
-          if (info.Options.TestGenOptions.Verbose) {
+          if (info.Options.Verbose) {
             info.Options.OutputWriter.WriteLine($"// Values of type {newTypeName} will be " +
                                    $"assigned the default value of " +
                                    $"{Printer.ExprToString(info.Options, info.witnessForType[newTypeName])}");
           }
-        } else if (info.Options.TestGenOptions.Verbose) {
+        } else if (info.Options.Verbose) {
           var message = $@"
 *** Error: Values of type {newTypeName} 
 will be assigned a default value of type {baseType}, 

diff --git a/Source/DafnyTestGeneration/DeadCodeCommand.cs b/Source/DafnyTestGeneration/DeadCodeCommand.cs
@@ -33,7 +33,6 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
     dafnyOptions.ForceCompile = false;
-    dafnyOptions.Verbose = false;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
 

diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -38,40 +38,10 @@ private enum Mode {
   /// parameter in everything except the value of the ProcsToCheck field that
   /// determines the procedures to be verified and should be set to the value of
   /// the <param name="procedureToVerify"></param> parameter.
-  /// Note that this cannot be refactored to use the DafnyOptions.CopyTo method
-  /// because we have to modify ProcsToCheck list, which does not have a setter.
   /// </summary>
   internal static DafnyOptions CopyForProcedure(DafnyOptions options, string procedureToVerify) {
-    var copy = DafnyOptions.Create(options.OutputWriter, options.Input, new[] { "/proc:" + procedureToVerify });
-    // Options set by the user:
-    copy.LoopUnrollCount = options.LoopUnrollCount;
-    copy.TestGenOptions.SeqLengthLimit = options.TestGenOptions.SeqLengthLimit;
-    copy.TestGenOptions.TargetMethod = options.TestGenOptions.TargetMethod;
-    copy.ProverLogFilePath = options.ProverLogFilePath;
-    copy.ProverLogFileAppend = options.ProverLogFileAppend;
-    copy.ProverOptions.Clear();
-    copy.ProverOptions.AddRange(options.ProverOptions);
-    copy.ResourceLimit = options.ResourceLimit;
-    copy.TimeLimit = options.TimeLimit;
-    copy.ProverDllName = options.ProverDllName;
-    copy.TheProverFactory = options.TheProverFactory;
-    copy.TestGenOptions.Verbose = options.TestGenOptions.Verbose;
-    copy.TestGenOptions.PrintBpl = options.TestGenOptions.PrintBpl;
-    copy.TestGenOptions.DisablePrune = options.TestGenOptions.DisablePrune;
-    copy.Prune = !options.TestGenOptions.DisablePrune;
-    // Options set by default in PostProcess:
-    copy.CompilerName = options.CompilerName;
-    copy.Compile = options.Compile;
-    copy.RunAfterCompile = options.RunAfterCompile;
-    copy.ForceCompile = options.ForceCompile;
-    copy.Verbose = options.Verbose;
-    copy.DeprecationNoise = options.DeprecationNoise;
-    copy.ForbidNondeterminism = options.ForbidNondeterminism;
-    copy.DefiniteAssignmentLevel = options.DefiniteAssignmentLevel;
-    copy.TestGenOptions.Mode = options.TestGenOptions.Mode;
-    copy.TestGenOptions.WarnDeadCode = options.TestGenOptions.WarnDeadCode;
-    // Options that may be modified by Test Generation itself:
-    copy.VerifyAllModules = options.VerifyAllModules;
+    var copy = new DafnyOptions(options);
+    copy.ProcsToCheck = new List<string>() { procedureToVerify };
     return copy;
   }
 
@@ -93,7 +63,6 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
     dafnyOptions.ForceCompile = false;
-    dafnyOptions.Verbose = false;
     dafnyOptions.DeprecationNoise = 0;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
@@ -116,9 +85,6 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
   public static readonly Option<int> LoopUnroll = new("--loop-unroll",
     "Higher values can improve accuracy of the analysis at the cost of taking longer to run.") {
   };
-  public static readonly Option<bool> Verbose = new("--verbose",
-    "Print various debugging info as comments for the generated tests.") {
-  };
   public static readonly Option<string> PrintBpl = new("--print-bpl",
     "Print the Boogie code used during test generation.") {
     ArgumentHelpName = "filename"
@@ -136,9 +102,6 @@ static GenerateTestsCommand() {
     DafnyOptions.RegisterLegacyBinding(Target, (options, value) => {
       options.TestGenOptions.TargetMethod = value;
     });
-    DafnyOptions.RegisterLegacyBinding(Verbose, (options, value) => {
-      options.TestGenOptions.Verbose = value;
-    });
     DafnyOptions.RegisterLegacyBinding(PrintBpl, (options, value) => {
       options.TestGenOptions.PrintBpl = value;
     });
@@ -150,7 +113,6 @@ static GenerateTestsCommand() {
       LoopUnroll,
       SequenceLengthLimit,
       Target,
-      Verbose,
       PrintBpl,
       DisablePrune
     );

diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs
@@ -91,6 +91,7 @@ private static void SetupForCounterexamples(DafnyOptions options) {
       options.ErrorTrace = 1;
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
+      options.Prune = !options.TestGenOptions.DisablePrune;
     }
 
     /// <summary>
@@ -122,7 +123,7 @@ private static void SetupForCounterexamples(DafnyOptions options) {
       counterexampleStatus = Status.Failure;
       counterexampleLog = null;
       if (result is not Task<PipelineOutcome>) {
-        if (Options.TestGenOptions.Verbose) {
+        if (Options.Verbose) {
           await options.OutputWriter.WriteLineAsync(
             $"// No test can be generated for {uniqueId} " +
             "because the verifier timed out.");
@@ -138,13 +139,13 @@ await options.OutputWriter.WriteLineAsync(
           counterexampleStatus = Status.Success;
           var blockId = int.Parse(Regex.Replace(line, @"\s+", "").Split('|')[2]);
           coversBlocks.Add(blockId);
-          if (Options.TestGenOptions.Verbose &&
+          if (Options.Verbose &&
               Options.TestGenOptions.Mode != TestGenerationOptions.Modes.Path) {
             await options.OutputWriter.WriteLineAsync($"// Test {uniqueId} covers block {blockId}");
           }
         }
       }
-      if (Options.TestGenOptions.Verbose && counterexampleLog == null) {
+      if (Options.Verbose && counterexampleLog == null) {
         if (log == "") {
           await options.OutputWriter.WriteLineAsync(
             $"// No test is generated for {uniqueId} " +
@@ -164,7 +165,7 @@ await options.OutputWriter.WriteLineAsync(
     }
 
     public async Task<TestMethod> GetTestMethod(Modifications cache, DafnyInfo dafnyInfo, bool returnNullIfNotUnique = true) {
-      if (Options.TestGenOptions.Verbose) {
+      if (Options.Verbose) {
         await dafnyInfo.Options.OutputWriter.WriteLineAsync(
           $"// Extracting the test for {uniqueId} from the counterexample...");
       }
@@ -182,7 +183,7 @@ await dafnyInfo.Options.OutputWriter.WriteLineAsync(
       if (duplicate == null) {
         return testMethod;
       }
-      if (Options.TestGenOptions.Verbose) {
+      if (Options.Verbose) {
         await dafnyInfo.Options.OutputWriter.WriteLineAsync(
           $"// Test for {uniqueId} matches a test previously generated " +
           $"for {duplicate.uniqueId}. This happens when test generation tool " +

diff --git a/Source/DafnyTestGeneration/ProgramModifier.cs b/Source/DafnyTestGeneration/ProgramModifier.cs
@@ -339,7 +339,7 @@ private void GetCalleesRecursively(string caller, Dictionary<string, uint> recor
             continue;
           }
           recorded[callee] = toInline;
-          if (info.Options.TestGenOptions.Verbose) {
+          if (info.Options.Verbose) {
             Console.Out.WriteLine($"// Will inline calls to {callee} with recursion unrolling depth set to {toInline}.");
           }
           GetCalleesRecursively(callee, recorded);

diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs
@@ -675,7 +675,7 @@ private List<string> TestMethodLines() {
       List<string> lines = new();
 
       if (errorMessages.Count != 0) {
-        if (DafnyInfo.Options.TestGenOptions.Verbose) {
+        if (DafnyInfo.Options.Verbose) {
           lines.AddRange(errorMessages);
         }
         return lines;

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
@@ -340,8 +340,6 @@ Usage: dafny [ option ... ] [ filename ... ]
       If specified, only this method will be tested.
   /generateTestPrintBpl:<fileName>
       Print the Boogie code used during test generation.
-  /generateTestVerbose
-      Print various debugging info as comments for the generated tests.
   /generateTestNoPrune
       Disable axiom pruning that Dafny uses to speed up verification.
   ---- Compilation options ---------------------------------------------------

diff --git a/docs/dev/4146.fix b/docs/dev/4146.fix
@@ -0,0 +1 @@
+Remove redundant code in the test generation project