From 90f2ae09d29b841ff42cdd8f441bda684c3421e2 Mon Sep 17 00:00:00 2001 From: Shaobo Date: Fri, 30 Oct 2015 14:53:07 -0600 Subject: Added wild card matching for /proc flag --- Source/Core/CommandLineOptions.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f4cba1dc..d7644915 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -11,6 +11,7 @@ using System.IO; using System.Linq; using System.Diagnostics; using System.Diagnostics.Contracts; +using System.Text.RegularExpressions; namespace Microsoft.Boogie { public class CommandLineOptionEngine @@ -1700,7 +1701,7 @@ namespace Microsoft.Boogie { // no preference return true; } - return ProcsToCheck.Contains(methodFullname); + return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$")); } public virtual StringCollection ParseNamedArgumentList(string argList) { -- cgit v1.2.3 From 12c5ff0211e844156706f8e617c94ab221c1b456 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 31 Oct 2015 08:19:49 +0000 Subject: Added test cases for the new asterisk wildcard behaviour of the ``-proc`` command line argument. --- .../multiple_procs_unusual_identifiers.bpl | 75 ++++++++++++++++++++++ ...ultiple_procs_verify_four_asterisk_wildcard.bpl | 28 ++++++++ ...le_procs_verify_two_asterisk_wildcard_begin.bpl | 17 +++++ ...iple_procs_verify_two_asterisk_wildcard_end.bpl | 17 +++++ ...rocs_verify_two_asterisk_wildcard_inbetween.bpl | 23 +++++++ 5 files changed, 160 insertions(+) create mode 100644 Test/commandline/multiple_procs_unusual_identifiers.bpl create mode 100644 Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl create mode 100644 Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl create mode 100644 Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl create mode 100644 Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl diff --git a/Test/commandline/multiple_procs_unusual_identifiers.bpl b/Test/commandline/multiple_procs_unusual_identifiers.bpl new file mode 100644 index 00000000..a3a4a4c1 --- /dev/null +++ b/Test/commandline/multiple_procs_unusual_identifiers.bpl @@ -0,0 +1,75 @@ +// RUN: %boogie "-proc:*Bar*" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 10 verified, 0 errors + +procedure foo() +{ + assert false; +} + +procedure bar() +{ + assert false; +} + +/* Start should be matched */ + +procedure _Bar() +{ + assert true; +} + +procedure .Bar() +{ + assert true; +} + +procedure ..Bar..() +{ + assert true; +} + +procedure $Bar() +{ + assert true; +} + +procedure #Bar() +{ + assert true; +} + +procedure 'Bar''() +{ + assert true; +} + +procedure ``Bar``() +{ + assert true; +} + +procedure ~Bar() +{ + assert true; +} + +procedure Bar^^() +{ + assert true; +} + +/* This is Boogie2 claims backslash is a valid identifier + but the parser rejects this. +procedure Bar\\() +{ + assert true; +} +*/ + +procedure ??Bar() +{ + assert true; +} + +/* End should be matched */ diff --git a/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl new file mode 100644 index 00000000..e0f8eef3 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie "-proc:*Bar" "-proc:*Foo" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 4 verified, 0 errors + +procedure foo() +{ + assert false; +} + +procedure helpfulFoo() +{ + assert true; +} + +procedure Foo() +{ + assert true; +} + +procedure translucentBar() +{ + assert true; +} + +procedure opaqueBar() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl new file mode 100644 index 00000000..0f6571ba --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "-proc:*Bar" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +procedure translucentBar() +{ + assert true; +} + +procedure opaqueBar() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl new file mode 100644 index 00000000..5cb102e2 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "-proc:bar*" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +procedure bar() +{ + assert true; +} + +procedure barzzz() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl new file mode 100644 index 00000000..7e19fe79 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie "-proc:trivial*ZZZ" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +// should not be matched +procedure trivialFooZZX() +{ + assert false; +} + +procedure trivialFooZZZ() +{ + assert true; +} + +procedure trivialBarZZZ() +{ + assert true; +} -- cgit v1.2.3 From 8d1864f189552068d22f174b6eeaee202568de36 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 31 Oct 2015 08:52:02 +0000 Subject: Document the new behaviour of the ``-proc:`` command line option in the output of Boogie's help. --- Source/Core/CommandLineOptions.cs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d7644915..3892bbc0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1858,7 +1858,15 @@ namespace Microsoft.Boogie { Multiple .bpl files supplied on the command line are concatenated into one Boogie program. - /proc:

: limits which procedures to check + /proc:

: Only check procedures matched by pattern

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

matches the whole procedure name (i.e. + pattern ""foo"" will only match a procedure called foo and + not fooBar). The pattern

may contain * wildcards which + match any character zero or more times. For example the + pattern ""ab*d"" would match abd, abcd and abccd but not + Aabd nor abdD. The pattern ""*ab*d*"" would match abd, + abcd, abccd, Abd and abdD. /noResolve : parse only /noTypecheck : parse and resolve only -- cgit v1.2.3