From 5b6a6e266c32f211c9f1ceff1d9605592b2016dd Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 17 Dec 2010 00:33:23 +0000
Subject: Add new feature: {:selective_checking} on procedures. See testcase
 for a description (it was implemented in VCC before and is quite useful).

---
 Test/test2/Answer                | 18 +++++++++++++++
 Test/test2/SelectiveChecking.bpl | 49 ++++++++++++++++++++++++++++++++++++++++
 Test/test2/runtest.bat           |  2 +-
 3 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 Test/test2/SelectiveChecking.bpl

(limited to 'Test/test2')

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
-- 
cgit v1.2.3