Add new feature: {:selective_checking} on procedures. See testcase for a description (it was implemented in VCC before and is quite useful).

3 files changed, 68 insertions, 1 deletions

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 4c0cbfc1..ca050273 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -381,6 +381,24 @@ Execution trace:
 

 Boogie program verifier finished with 1 verified, 3 errors

 

+-------------------- SelectiveChecking.bpl --------------------

+SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    SelectiveChecking.bpl(15,3): anon0

+SelectiveChecking.bpl(30,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    SelectiveChecking.bpl(24,3): anon0

+    SelectiveChecking.bpl(27,5): anon3_Then

+    SelectiveChecking.bpl(30,3): anon2

+SelectiveChecking.bpl(37,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    SelectiveChecking.bpl(37,3): anon0

+SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    SelectiveChecking.bpl(37,3): anon0

+

+Boogie program verifier finished with 1 verified, 4 errors

+

 -------------------- Arrays.bpl /typeEncoding:m --------------------

 Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.

 Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.

diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl
new file mode 100644
index 00000000..2f08618a
--- /dev/null
+++ b/Test/test2/SelectiveChecking.bpl
@@ -0,0 +1,49 @@
+/*
+In functions marked with {:selective_checking} all asserts are turned into assumes,
+except for the ones reachable from the commands marked with {:start_checking_here}.
+Thus, "assume {:start_checking_here} whatever;" is an inverse of "assume false;".
+The first one disables all verification before it, and the second one disables
+all verification after.
+*/
+
+procedure {:selective_checking} foo()
+{
+  var x, y, z : int;
+
+  assert x < y;
+  assert y < z;
+  assume {:start_checking_here} true;
+  assert x < z;
+}
+
+procedure {:selective_checking} foo_fail1()
+{
+  var x, y, z : int;
+
+  assert x < y;
+  assume {:start_checking_here} true;
+  assert x < z;
+}
+
+procedure {:selective_checking} foo_fail2()
+{
+  var x, y, z : int;
+
+  assert x < y;
+  
+  if (*) {
+    assume {:start_checking_here} true;
+  }
+
+  assert x < z;
+}
+
+procedure foo_no_selch()
+{
+  var x, y, z : int;
+
+  assert x < y;
+  assume {:start_checking_here} true;
+  assert x < z;
+}
+
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index f704e263..c9d4feac 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             strings-no-where.bpl strings-where.bpl

             Structured.bpl Where.bpl UpdateExpr.bpl

             NeverPattern.bpl NullaryMaps.bpl Implies.bpl

-	    IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl) do (

+	    IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /noinfer %%f