diff options
author | wuestholz <unknown> | 2014-10-28 17:09:16 +0100 |
---|---|---|
committer | wuestholz <unknown> | 2014-10-28 17:09:16 +0100 |
commit | 0bf625b0c480624e4fa36663bd443d9f1db08c09 (patch) | |
tree | b03c4d699c06e3683b91f49d4d68578083239d76 | |
parent | fe2e342ca13313ec1f3bf4e3b3c27e641dfb1d93 (diff) |
Fixed minor issue (reported by Alex Summers).
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index eca410b2..f938b0f8 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -147,12 +147,22 @@ namespace Microsoft.Boogie { /// </summary>
public bool GetNumericArgument(ref int arg) {
//modifies nextIndex, encounteredErrors, Console.Error.*;
+ return GetNumericArgument(ref arg, a => 0 <= a);
+ }
+
+ /// <summary>
+ /// If there is one argument and the filtering predicate holds, then set "arg" to that number and return "true".
+ /// Otherwise, emit error message, leave "arg" unchanged, and return "false".
+ /// </summary>
+ public bool GetNumericArgument(ref int arg, Predicate<int> filter) {
+ Contract.Requires(filter != null);
+
if (this.ConfirmArgumentCount(1)) {
try {
Contract.Assume(args[i] != null);
Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent
int d = Convert.ToInt32(this.args[this.i]);
- if (0 <= d) {
+ if (filter == null || filter(d)) {
arg = d;
return true;
}
@@ -1291,7 +1301,7 @@ namespace Microsoft.Boogie { return true;
case "vcsCores":
- ps.GetNumericArgument(ref VcsCores);
+ ps.GetNumericArgument(ref VcsCores, a => 1 <= a);
return true;
case "vcsLoad":
|