From 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 28 Jun 2015 02:19:12 +0100
Subject: Fix issue #16 reported by @crazykt

Previously when Boogie was passed the ``-proc:<NAME>`` argument on the command
line it would verify any procedure whose name contained ``<NAME>`` which
doesn't seem like correct behaviour.

Now Boogie only tries to verify a procedure only if its name matches
``<NAME>`` exactly. I've added several test cases to check Boogie
behaves as expected.
---
 Source/Core/CommandLineOptions.cs                  |  2 +-
 Test/commandline/multiple_procs_verify_one.bpl     | 22 ++++++++++++++++++++++
 .../multiple_procs_verify_one_request_twice.bpl    | 20 ++++++++++++++++++++
 Test/commandline/multiple_procs_verify_two.bpl     | 17 +++++++++++++++++
 4 files changed, 60 insertions(+), 1 deletion(-)
 create mode 100644 Test/commandline/multiple_procs_verify_one.bpl
 create mode 100644 Test/commandline/multiple_procs_verify_one_request_twice.bpl
 create mode 100644 Test/commandline/multiple_procs_verify_two.bpl

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 1c7f40d4..2be1cdf7 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1700,7 +1700,7 @@ namespace Microsoft.Boogie {
         // no preference
         return true;
       }
-      return ProcsToCheck.Any(s => 0 <= methodFullname.IndexOf(s));
+      return ProcsToCheck.Contains(methodFullname);
     }
 
     public virtual StringCollection ParseNamedArgumentList(string argList) {
diff --git a/Test/commandline/multiple_procs_verify_one.bpl b/Test/commandline/multiple_procs_verify_one.bpl
new file mode 100644
index 00000000..eaaa9af4
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_one.bpl
@@ -0,0 +1,22 @@
+// RUN: %boogie -proc:foo "%s" > "%t"
+// RUN: %OutputCheck --file-to-check %t %s
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+// Only this procedure should be verified, the others should be ignored
+procedure foo()
+{
+    assume true;
+}
+
+// An old version of Boogie just checked if the name passed to ``-proc:``
+// occurs somewhere in procedure name which would cause it to try and also
+// verify the procedures below.
+procedure foo2()
+{
+    assert false;
+}
+
+procedure function_foo()
+{
+    assert false;
+}
diff --git a/Test/commandline/multiple_procs_verify_one_request_twice.bpl b/Test/commandline/multiple_procs_verify_one_request_twice.bpl
new file mode 100644
index 00000000..fe9c44ba
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_one_request_twice.bpl
@@ -0,0 +1,20 @@
+// RUN: %boogie -proc:foo -proc:foo "%s" > "%t"
+// RUN: %OutputCheck --file-to-check %t %s
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+// Although the command line requests two verify this procedure twice we should
+// only do try once.
+procedure foo()
+{
+    assume true;
+}
+
+procedure bar()
+{
+    assert false;
+}
+
+procedure baz()
+{
+    assert false;
+}
diff --git a/Test/commandline/multiple_procs_verify_two.bpl b/Test/commandline/multiple_procs_verify_two.bpl
new file mode 100644
index 00000000..9e3fb0c6
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie -proc:foo -proc:bar "%s" > "%t"
+// RUN: %OutputCheck --file-to-check %t %s
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+    assume true;
+}
+
+procedure bar()
+{
+    assert true;
+}
+
+procedure barz()
+{
+    assert false;
+}
-- 
cgit v1.2.3