summaryrefslogtreecommitdiff
path: root/Source/Core/CommandLineOptions.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
-rw-r--r--Source/Core/CommandLineOptions.cs13
1 files changed, 11 insertions, 2 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index f4cba1dc..3892bbc0 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) {
@@ -1857,7 +1858,15 @@ namespace Microsoft.Boogie {
Multiple .bpl files supplied on the command line are concatenated into one
Boogie program.
- /proc:<p> : limits which procedures to check
+ /proc:<p> : Only check procedures matched by pattern <p>. This option
+ may be specified multiple times to match multiple patterns.
+ The pattern <p> matches the whole procedure name (i.e.
+ pattern ""foo"" will only match a procedure called foo and
+ not fooBar). The pattern <p> 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