diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 274c2bb4424..8e3726465e5 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -10,13 +10,6 @@ namespace Microsoft.Dafny; public static class BoogieOptionBag { - public static readonly Option> BoogieFilter = new("--boogie-filter", @" -(obsolete, use --filter-symbol instead) Only check proofs whose Boogie name is matched by pattern

. This option may be specified multiple times to match multiple patterns. The pattern

may contain * wildcards which match any character zero or more times. If you are unsure of how Boogie names are generated, please pre- and postfix your pattern with a wildcard to enable matching on Dafny proof names." - .TrimStart()) { - ArgumentHelpName = "pattern", - IsHidden = true, - }; - public static readonly Option> BoogieArguments = new("--boogie", "Specify arguments that are passed to Boogie, a tool used to verify Dafny programs.") { ArgumentHelpName = "arguments", @@ -103,7 +96,6 @@ public static class BoogieOptionBag { static BoogieOptionBag() { Cores.SetDefaultValue((uint)((Environment.ProcessorCount + 1) / 2)); - DafnyOptions.RegisterLegacyBinding(BoogieFilter, (o, f) => o.ProcsToCheck.AddRange(f)); DafnyOptions.RegisterLegacyBinding(BoogieArguments, (o, boogieOptions) => { var splitOptions = boogieOptions.SelectMany(SplitArguments).ToArray(); if (splitOptions.Any()) { @@ -161,8 +153,7 @@ static BoogieOptionBag() { SolverOptionHelp, SolverPath, SolverPlugin, - SolverResourceLimit, - BoogieFilter + SolverResourceLimit ); } diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 65173a59896..660d28dce63 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -42,7 +42,6 @@ public static Command Create() { new Option[] { FilterSymbol, FilterPosition, - BoogieOptionBag.BoogieFilter, }.Concat(DafnyCommands.VerificationOptions). Concat(DafnyCommands.ConsoleOutputOptions). Concat(DafnyCommands.ResolverOptions); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3571.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3571.dfy index 52e4a5f3e1b..765e1ea12e1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3571.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3571.dfy @@ -14,6 +14,5 @@ // RUN: %diff "%s.expect" "%t" // Crashes size x is nothing real // ## %verify --solver-plugin x --solver-plugin x "%s" >> "%t" -// Not testing --boogi, --boogie-filter module A {} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy deleted file mode 100644 index 7fe96e730b4..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: %verify --boogie-filter='*Succeeds*' --bprint:"%t.bpl" %s > %t -// RUN: ! %verify %s >> %t -// RUN: %diff "%s.expect" "%t" - -method Succeeds() - ensures true { -} - -method Fails() - ensures false { -} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect deleted file mode 100644 index 0e083ce5590..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect +++ /dev/null @@ -1,6 +0,0 @@ - -Dafny program verifier finished with 1 verified, 0 errors -boogie-filter.dfy(10,16): Error: a postcondition could not be proved on this return path -boogie-filter.dfy(10,10): Related location: this is the postcondition that could not be proved - -Dafny program verifier finished with 1 verified, 1 error diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 0c4ec18adc1..4c1f2d49f38 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -280,12 +280,12 @@ Various options control the verification process, in addition to all those descr - `--relax-definite-assignment` - `--track-print-effects` - `--disable-nonlinear-arithmetic` + - `--filter-symbol` - Control of the proof engine - `--manual-lemma-induction` - `--verification-time-limit` - `--boogie` - - `--boogie-filter` - `--solver-path` @@ -2643,8 +2643,6 @@ terminology. * `--solver-plugin` - specifies a plugin to use as the SMT solver, instead of an external pdafny translaterocess -* `--boogie-filter` - restricts the set of verification tasks (for debugging) - * `--boogie` - arguments to send to boogie Legacy options: diff --git a/docs/dev/news/4816.feat b/docs/dev/news/4816.feat index 0981a67d518..7d26361249a 100644 --- a/docs/dev/news/4816.feat +++ b/docs/dev/news/4816.feat @@ -1,3 +1,3 @@ - Add an option `--filter-position` to the `dafny verify` command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with ``--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23` - -- Add an option `--filter-symbol` to the `dafny verify` command, that only verifies symbols whose fully qualified contains the given argument. For example, `dafny verify dfyconfig.toml --filter-symbol=MyModule` will verify everything inside `MyModule`. \ No newline at end of file +- Add an option `--filter-symbol` to the `dafny verify` command, that only verifies symbols whose fully qualified name contains the given argument. For example, `dafny verify dfyconfig.toml --filter-symbol=MyModule` will verify everything inside `MyModule`. +- The option `--boogie-filter` has been removed in favor of --filter-symbol \ No newline at end of file