Skip to content

Commit 8774643

Browse files
Remove boogie filter (#5090)
Fix for #5088 ### Description Remove `--boogie-filter` option, because there's now a better `--filter-symbol` ### How has this been tested? Tests for the removed feature have been removed. <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>
1 parent 28f3a62 commit 8774643

File tree

7 files changed

+4
-34
lines changed

7 files changed

+4
-34
lines changed

Source/DafnyCore/Options/BoogieOptionBag.cs

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,6 @@
1010
namespace Microsoft.Dafny;
1111

1212
public static class BoogieOptionBag {
13-
public static readonly Option<IEnumerable<string>> BoogieFilter = new("--boogie-filter", @"
14-
(obsolete, use --filter-symbol instead) Only check proofs whose Boogie name is matched by pattern <p>. This option may be specified multiple times to match multiple patterns. The pattern <p> 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."
15-
.TrimStart()) {
16-
ArgumentHelpName = "pattern",
17-
IsHidden = true,
18-
};
19-
2013
public static readonly Option<IEnumerable<string>> BoogieArguments = new("--boogie",
2114
"Specify arguments that are passed to Boogie, a tool used to verify Dafny programs.") {
2215
ArgumentHelpName = "arguments",
@@ -103,7 +96,6 @@ public static class BoogieOptionBag {
10396
static BoogieOptionBag() {
10497
Cores.SetDefaultValue((uint)((Environment.ProcessorCount + 1) / 2));
10598

106-
DafnyOptions.RegisterLegacyBinding(BoogieFilter, (o, f) => o.ProcsToCheck.AddRange(f));
10799
DafnyOptions.RegisterLegacyBinding(BoogieArguments, (o, boogieOptions) => {
108100
var splitOptions = boogieOptions.SelectMany(SplitArguments).ToArray();
109101
if (splitOptions.Any()) {
@@ -161,8 +153,7 @@ static BoogieOptionBag() {
161153
SolverOptionHelp,
162154
SolverPath,
163155
SolverPlugin,
164-
SolverResourceLimit,
165-
BoogieFilter
156+
SolverResourceLimit
166157
);
167158
}
168159

Source/DafnyDriver/Commands/VerifyCommand.cs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,6 @@ public static Command Create() {
4242
new Option[] {
4343
FilterSymbol,
4444
FilterPosition,
45-
BoogieOptionBag.BoogieFilter,
4645
}.Concat(DafnyCommands.VerificationOptions).
4746
Concat(DafnyCommands.ConsoleOutputOptions).
4847
Concat(DafnyCommands.ResolverOptions);

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3571.dfy

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,5 @@
1414
// RUN: %diff "%s.expect" "%t"
1515
// Crashes size x is nothing real
1616
// ## %verify --solver-plugin x --solver-plugin x "%s" >> "%t"
17-
// Not testing --boogi, --boogie-filter
1817

1918
module A {}

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy

Lines changed: 0 additions & 11 deletions
This file was deleted.

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/boogie-filter.dfy.expect

Lines changed: 0 additions & 6 deletions
This file was deleted.

docs/DafnyRef/UserGuide.md

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -280,12 +280,12 @@ Various options control the verification process, in addition to all those descr
280280
- `--relax-definite-assignment`
281281
- `--track-print-effects`
282282
- `--disable-nonlinear-arithmetic`
283+
- `--filter-symbol`
283284

284285
- Control of the proof engine
285286
- `--manual-lemma-induction`
286287
- `--verification-time-limit`
287288
- `--boogie`
288-
- `--boogie-filter`
289289
- `--solver-path`
290290

291291

@@ -2643,8 +2643,6 @@ terminology.
26432643

26442644
* `--solver-plugin` - specifies a plugin to use as the SMT solver, instead of an external pdafny translaterocess
26452645

2646-
* `--boogie-filter` - restricts the set of verification tasks (for debugging)
2647-
26482646
* `--boogie` - arguments to send to boogie
26492647

26502648
Legacy options:

docs/dev/news/4816.feat

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
- 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`
2-
3-
- 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`.
2+
- 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`.
3+
- The option `--boogie-filter` has been removed in favor of --filter-symbol

0 commit comments

Comments
 (0)