From 4438bfb9b3974958dac6be894b5446d582b65fac Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 16 Nov 2022 12:38:09 +0100 Subject: [PATCH 01/15] Add check-stability command --- .../DafnyDriver/Commands/CommandRegistry.cs | 1 + .../DafnyDriver/Commands/StabilityCommand.cs | 94 +++++++++++++++++++ 2 files changed, 95 insertions(+) create mode 100644 Source/DafnyDriver/Commands/StabilityCommand.cs diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index d50122d2506..3e14998e561 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -45,6 +45,7 @@ static CommandRegistry() { AddCommand(new RunCommand()); AddCommand(new BuildCommand()); AddCommand(new TranslateCommand()); + AddCommand(new StabilityCommand()); FileArgument = new Argument("file", "input file"); FileArgument.AddValidator(ValidateFileArgument()); diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs new file mode 100644 index 00000000000..276da762d9e --- /dev/null +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -0,0 +1,94 @@ +using System.Collections.Generic; +using System.CommandLine; +using System.CommandLine.Invocation; +using System.Linq; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +public class StabilityCommand : ICommandSpec { + public IEnumerable Options => new IOptionSpec[] { + IterationsOption.Instance, + RandomSeedOption.Instance, + FormatOption.Instance, + IsolateAssertionsOption.Instance, + }.Concat(CommandRegistry.CommonOptions); + + public Command Create() { + var result = new Command("check-stability", "(experimental) Check the stability of the program proofs. Be aware that the options and output of this command will change in the future."); + result.AddArgument(CommandRegistry.FilesArgument); + return result; + } + + public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) { + } +} + +class IsolateAssertionsOption : BooleanOption { + public static readonly IsolateAssertionsOption Instance = new (); + public override string LongName => "isolate-assertions"; + + public override string Description => @"Verify each assertion in isolation."; + + public override string PostProcess(DafnyOptions options) { + options.VcsSplitOnEveryAssert = Get(options); + return null; + } +} + +class FormatOption : CommandLineOption> { + public static readonly FormatOption Instance = new (); + public override object DefaultValue => Enumerable.Empty(); + + public override string LongName => "format"; + public override string ArgumentName => "configuration"; + + public override string Description => $@" +Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format:trx;LogFileName=<...>.z + +The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option. + + The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the`{IsolateAssertionsOption.Instance.LongName}` option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart(); + + public override string PostProcess(DafnyOptions options) { + options.VerificationLoggerConfigs = Get(options).ToList(); + return null; + } + + public override void Parse(CommandLineParseState ps, DafnyOptions options) { + throw new System.NotImplementedException(); + } +} + +class RandomSeedOption : NaturalNumberOption { + public static readonly RandomSeedOption Instance = new (); + public override object DefaultValue => 0U; + public override string LongName => "random-seed"; + public override string ArgumentName => "seed"; + + public override string Description => + $"Turn on randomization of the input that Boogie passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Boogie inputs are unstable in the sense that changes to the input that preserve its meaning may cause the output to change. This option simulates meaning-preserving changes to the input without requiring the user to actually make those changes. The input changes are renaming variables and reordering declarations in the input, and setting solver options that have similar effects."; + + public override string PostProcess(DafnyOptions options) { + if (Get(options) != (ulong)DefaultValue) { + options.RandomSeed = (int?)Get(options); + } + + return null; + } +} + +class IterationsOption : NaturalNumberOption { + public static readonly IterationsOption Instance = new (); + public override object DefaultValue => 10; + public override string LongName => "iterations"; + public override string ArgumentName => "n"; + + public override string Description => + $"Attempt to verify each proof n times with n random seeds. If {RandomSeedOption.Instance.LongName} is used, each proof attempt will use a new random seed derived from this one. If not, it will use a different seed between iterations."; + + public override string PostProcess(DafnyOptions options) { + options.RandomSeedIterations = (int)Get(options); + return null; + } +} From 0cf53df7fc306598a554f9582f05f41fd64100b1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 16 Nov 2022 12:38:33 +0100 Subject: [PATCH 02/15] Run formatter --- Source/DafnyDriver/Commands/StabilityCommand.cs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs index 276da762d9e..2095c714335 100644 --- a/Source/DafnyDriver/Commands/StabilityCommand.cs +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -25,7 +25,7 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo } class IsolateAssertionsOption : BooleanOption { - public static readonly IsolateAssertionsOption Instance = new (); + public static readonly IsolateAssertionsOption Instance = new(); public override string LongName => "isolate-assertions"; public override string Description => @"Verify each assertion in isolation."; @@ -37,7 +37,7 @@ public override string PostProcess(DafnyOptions options) { } class FormatOption : CommandLineOption> { - public static readonly FormatOption Instance = new (); + public static readonly FormatOption Instance = new(); public override object DefaultValue => Enumerable.Empty(); public override string LongName => "format"; @@ -61,7 +61,7 @@ public override void Parse(CommandLineParseState ps, DafnyOptions options) { } class RandomSeedOption : NaturalNumberOption { - public static readonly RandomSeedOption Instance = new (); + public static readonly RandomSeedOption Instance = new(); public override object DefaultValue => 0U; public override string LongName => "random-seed"; public override string ArgumentName => "seed"; @@ -79,7 +79,7 @@ public override string PostProcess(DafnyOptions options) { } class IterationsOption : NaturalNumberOption { - public static readonly IterationsOption Instance = new (); + public static readonly IterationsOption Instance = new(); public override object DefaultValue => 10; public override string LongName => "iterations"; public override string ArgumentName => "n"; From c2b268e8df06b81dac6132826bebf1d1a625a566 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 16 Nov 2022 12:42:17 +0100 Subject: [PATCH 03/15] Update tests --- Source/DafnyDriver/Commands/StabilityCommand.cs | 2 +- Test/logger/CSVLogger.dfy | 2 +- Test/logger/TextLogger.dfy | 2 +- Test/logger/TextLoggerBatch.dfy | 2 +- Test/logger/VerificationLogger.dfy | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs index 2095c714335..352122f2bba 100644 --- a/Source/DafnyDriver/Commands/StabilityCommand.cs +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -48,7 +48,7 @@ class FormatOption : CommandLineOption> { The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option. - The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the`{IsolateAssertionsOption.Instance.LongName}` option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart(); +The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the`{IsolateAssertionsOption.Instance.LongName}` option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart(); public override string PostProcess(DafnyOptions options) { options.VerificationLoggerConfigs = Get(options).ToList(); diff --git a/Test/logger/CSVLogger.dfy b/Test/logger/CSVLogger.dfy index d06bc375e24..20d382fd36b 100644 --- a/Test/logger/CSVLogger.dfy +++ b/Test/logger/CSVLogger.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny_0 /verificationLogger:csv";"LogFileName="%t.csv" "%s" +// RUN: %baredafny check-stability --format:csv";"LogFileName="%t.csv" "%s" // RUN: %OutputCheck --file-to-check "%t.csv" "%s" // CHECK: TestResult\.DisplayName,TestResult\.Outcome,TestResult\.Duration,TestResult\.ResourceCount diff --git a/Test/logger/TextLogger.dfy b/Test/logger/TextLogger.dfy index ee5ba8adbe6..84eea3b67b7 100644 --- a/Test/logger/TextLogger.dfy +++ b/Test/logger/TextLogger.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny_0 /compile:0 /verificationLogger:text /vcsSplitOnEveryAssert "%s" > "%t" +// RUN: %baredafny check-stability --format:text --isolate-assertions "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Overall outcome: Errors // CHECK: Overall time: .* diff --git a/Test/logger/TextLoggerBatch.dfy b/Test/logger/TextLoggerBatch.dfy index 6634b5b8b68..3fbc0439d41 100644 --- a/Test/logger/TextLoggerBatch.dfy +++ b/Test/logger/TextLoggerBatch.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny_0 /compile:0 /verificationLogger:text "%s" > "%t" +// RUN: %baredafny check-stability --format:text "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Overall outcome: Errors // CHECK: Overall time: .* diff --git a/Test/logger/VerificationLogger.dfy b/Test/logger/VerificationLogger.dfy index 42d3e4d0c27..ec41c2cd378 100644 --- a/Test/logger/VerificationLogger.dfy +++ b/Test/logger/VerificationLogger.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny_0 /verificationLogger:trx";"LogFileName="%t.trx" "%s" +// RUN: %baredafny check-stability --format:trx";"LogFileName="%t.trx" "%s" // RUN: %OutputCheck --file-to-check "%t.trx" "%s" // CHECK: \ From 8b0ef0aa22e4b633d9d848b24ef1f8a24ac9f06e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 16 Nov 2022 12:45:39 +0100 Subject: [PATCH 04/15] Fix test --- Source/DafnyDriver/Commands/StabilityCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs index 352122f2bba..99df2c40a26 100644 --- a/Source/DafnyDriver/Commands/StabilityCommand.cs +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -48,7 +48,7 @@ class FormatOption : CommandLineOption> { The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option. -The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the`{IsolateAssertionsOption.Instance.LongName}` option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart(); +The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the {IsolateAssertionsOption.Instance.LongName}git d option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart(); public override string PostProcess(DafnyOptions options) { options.VerificationLoggerConfigs = Get(options).ToList(); From 0d408f449604915b3a326936e6d6f7b564cf6aff Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 16 Nov 2022 13:59:29 +0100 Subject: [PATCH 05/15] Fix text and default value --- Source/DafnyDriver/Commands/StabilityCommand.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs index 99df2c40a26..7e1b923ce71 100644 --- a/Source/DafnyDriver/Commands/StabilityCommand.cs +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -15,7 +15,7 @@ public class StabilityCommand : ICommandSpec { }.Concat(CommandRegistry.CommonOptions); public Command Create() { - var result = new Command("check-stability", "(experimental) Check the stability of the program proofs. Be aware that the options and output of this command will change in the future."); + var result = new Command("check-stability", "(experimental) Check the stability of the program proofs. Be aware that the name, options and output of this command will change in the future."); result.AddArgument(CommandRegistry.FilesArgument); return result; } @@ -80,7 +80,7 @@ public override string PostProcess(DafnyOptions options) { class IterationsOption : NaturalNumberOption { public static readonly IterationsOption Instance = new(); - public override object DefaultValue => 10; + public override object DefaultValue => 10U; public override string LongName => "iterations"; public override string ArgumentName => "n"; From b65f8f42bb61c38fd0d5576783d5fd1a197af38d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 16 Nov 2022 15:10:04 +0100 Subject: [PATCH 06/15] Fix cast and tests --- Source/DafnyDriver/Commands/StabilityCommand.cs | 2 +- Test/logger/CSVLogger.dfy | 2 +- Test/logger/TextLogger.dfy | 2 +- Test/logger/TextLoggerBatch.dfy | 2 +- Test/logger/VerificationLogger.dfy | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs index 7e1b923ce71..bef352b3d1c 100644 --- a/Source/DafnyDriver/Commands/StabilityCommand.cs +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -70,7 +70,7 @@ class RandomSeedOption : NaturalNumberOption { $"Turn on randomization of the input that Boogie passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Boogie inputs are unstable in the sense that changes to the input that preserve its meaning may cause the output to change. This option simulates meaning-preserving changes to the input without requiring the user to actually make those changes. The input changes are renaming variables and reordering declarations in the input, and setting solver options that have similar effects."; public override string PostProcess(DafnyOptions options) { - if (Get(options) != (ulong)DefaultValue) { + if (Get(options) != (uint)DefaultValue) { options.RandomSeed = (int?)Get(options); } diff --git a/Test/logger/CSVLogger.dfy b/Test/logger/CSVLogger.dfy index 20d382fd36b..2a4273426ab 100644 --- a/Test/logger/CSVLogger.dfy +++ b/Test/logger/CSVLogger.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny check-stability --format:csv";"LogFileName="%t.csv" "%s" +// RUN: %baredafny check-stability --format:csv";"LogFileName="%t.csv" "%s" || true // RUN: %OutputCheck --file-to-check "%t.csv" "%s" // CHECK: TestResult\.DisplayName,TestResult\.Outcome,TestResult\.Duration,TestResult\.ResourceCount diff --git a/Test/logger/TextLogger.dfy b/Test/logger/TextLogger.dfy index 84eea3b67b7..b94492d9a35 100644 --- a/Test/logger/TextLogger.dfy +++ b/Test/logger/TextLogger.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny check-stability --format:text --isolate-assertions "%s" > "%t" +// RUN: %baredafny check-stability --format:text --isolate-assertions "%s" > "%t" || true // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Overall outcome: Errors // CHECK: Overall time: .* diff --git a/Test/logger/TextLoggerBatch.dfy b/Test/logger/TextLoggerBatch.dfy index 3fbc0439d41..a5873471043 100644 --- a/Test/logger/TextLoggerBatch.dfy +++ b/Test/logger/TextLoggerBatch.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny check-stability --format:text "%s" > "%t" +// RUN: %baredafny check-stability --format:text "%s" > "%t" || true // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Overall outcome: Errors // CHECK: Overall time: .* diff --git a/Test/logger/VerificationLogger.dfy b/Test/logger/VerificationLogger.dfy index ec41c2cd378..1d264b695fa 100644 --- a/Test/logger/VerificationLogger.dfy +++ b/Test/logger/VerificationLogger.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny check-stability --format:trx";"LogFileName="%t.trx" "%s" +// RUN: %baredafny check-stability --format:trx";"LogFileName="%t.trx" "%s" || true // RUN: %OutputCheck --file-to-check "%t.trx" "%s" // CHECK: \ From 718b34430ac86ac9406bfc30aa16a5e0aa268031 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Nov 2022 15:01:13 +0100 Subject: [PATCH 07/15] Update Source/DafnyDriver/Commands/StabilityCommand.cs Co-authored-by: Aaron Tomb --- Source/DafnyDriver/Commands/StabilityCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/Commands/StabilityCommand.cs b/Source/DafnyDriver/Commands/StabilityCommand.cs index bef352b3d1c..153a7e923f0 100644 --- a/Source/DafnyDriver/Commands/StabilityCommand.cs +++ b/Source/DafnyDriver/Commands/StabilityCommand.cs @@ -44,7 +44,7 @@ class FormatOption : CommandLineOption> { public override string ArgumentName => "configuration"; public override string Description => $@" -Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format:trx;LogFileName=<...>.z +Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format "trx;LogFileName=<...>.z" The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option. From bbfdd4885a94b854c2477200e41063801dc1089b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 1 Dec 2022 16:12:44 +0100 Subject: [PATCH 08/15] Textual changes --- Source/DafnyDriver/Commands/ProofComplexityCommand.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyDriver/Commands/ProofComplexityCommand.cs b/Source/DafnyDriver/Commands/ProofComplexityCommand.cs index 05eb62f5a62..2c54f380c2e 100644 --- a/Source/DafnyDriver/Commands/ProofComplexityCommand.cs +++ b/Source/DafnyDriver/Commands/ProofComplexityCommand.cs @@ -45,7 +45,7 @@ class FormatOption : CommandLineOption> { public override string ArgumentName => "configuration"; public override string Description => $@" -Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format "trx;LogFileName=<...>.z" +Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format ""trx;LogFileName=<...>.z"" The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option. @@ -68,7 +68,7 @@ class RandomSeedOption : NaturalNumberOption { public override string ArgumentName => "seed"; public override string Description => - $"Turn on randomization of the input that Boogie passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Boogie inputs are unstable in the sense that changes to the input that preserve its meaning may cause the output to change. This option simulates meaning-preserving changes to the input without requiring the user to actually make those changes. The input changes are renaming variables and reordering declarations in the input, and setting solver options that have similar effects."; + $"Turn on randomization of the input that Dafny passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Dafny proofs are complex in the sense that changes to the proof that preserve its meaning may cause its verification result to change. This option simulates meaning-preserving changes to the proofs without requiring the user to actually make those changes. The proof changes are renaming variables and reordering declarations in the SMT input passed to the solver, and setting solver options that have similar effects."; public override string PostProcess(DafnyOptions options) { if (Get(options) != (uint)DefaultValue) { @@ -86,7 +86,7 @@ class IterationsOption : NaturalNumberOption { public override string ArgumentName => "n"; public override string Description => - $"Attempt to verify each proof n times with n random seeds. If {RandomSeedOption.Instance.LongName} is used, each proof attempt will use a new random seed derived from this one. If not, it will use a different seed between iterations."; + $"Attempt to verify each proof n times with n random seeds, each seed derived from the previous one. {RandomSeedOption.Instance.LongName} can be used to specify the first seed, which will otherwise be 0."; public override string PostProcess(DafnyOptions options) { options.RandomSeedIterations = (int)Get(options); From c31cbe5139cee647907b10962cde66947457e13f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 12 Dec 2022 19:22:20 +0100 Subject: [PATCH 09/15] Rename command name --- Source/DafnyDriver/Commands/ProofComplexityCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/Commands/ProofComplexityCommand.cs b/Source/DafnyDriver/Commands/ProofComplexityCommand.cs index e62c77f96a7..81c2f9e41e7 100644 --- a/Source/DafnyDriver/Commands/ProofComplexityCommand.cs +++ b/Source/DafnyDriver/Commands/ProofComplexityCommand.cs @@ -39,7 +39,7 @@ static ProofComplexityCommand() { }; public Command Create() { - var result = new Command("check-proof-complexity", "(experimental) Check the complexity of the program proofs. Be aware that the name, options and output of this command will change in the future."); + var result = new Command("check-proof-durability", "(experimental) Check the durability of the program proofs. Be aware that the name, options and output of this command will change in the future."); result.AddArgument(ICommandSpec.FilesArgument); return result; } From f9d453df0294c6b2168f1f08771cd27d26461ad3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 13 Dec 2022 11:47:48 +0100 Subject: [PATCH 10/15] Use all the options in tests --- Source/DafnyDriver/Commands/CommandRegistry.cs | 2 +- ...ityCommand.cs => ProofDurabilityCommand.cs} | 18 ++++++++++-------- Test/logger/VerificationLogger.dfy | 2 +- 3 files changed, 12 insertions(+), 10 deletions(-) rename Source/DafnyDriver/Commands/{ProofComplexityCommand.cs => ProofDurabilityCommand.cs} (87%) diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 51265c11e3e..c04206d5bcc 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -30,7 +30,7 @@ static CommandRegistry() { AddCommand(new RunCommand()); AddCommand(new BuildCommand()); AddCommand(new TranslateCommand()); - AddCommand(new ProofComplexityCommand()); + AddCommand(new ProofDurabilityCommand()); AddCommand(new ServerCommand()); AddCommand(new TestCommand()); AddCommand(new GenerateTestsCommand()); diff --git a/Source/DafnyDriver/Commands/ProofComplexityCommand.cs b/Source/DafnyDriver/Commands/ProofDurabilityCommand.cs similarity index 87% rename from Source/DafnyDriver/Commands/ProofComplexityCommand.cs rename to Source/DafnyDriver/Commands/ProofDurabilityCommand.cs index 81c2f9e41e7..846c04e5bb1 100644 --- a/Source/DafnyDriver/Commands/ProofComplexityCommand.cs +++ b/Source/DafnyDriver/Commands/ProofDurabilityCommand.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; -public class ProofComplexityCommand : ICommandSpec { +public class ProofDurabilityCommand : ICommandSpec { public IEnumerable