From c250f55e7af88a3671262e2c0522664f299ef2f2 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 14 Sep 2011 16:28:25 +0200
Subject: Added "free call" statements that don't check the precondition in the
 caller.

---
 Test/test2/Answer       | 23 ++++++++++++
 Test/test2/FreeCall.bpl | 96 +++++++++++++++++++++++++++++++++++++++++++++++++
 Test/test2/runtest.bat  |  4 +--
 3 files changed, 121 insertions(+), 2 deletions(-)
 create mode 100644 Test/test2/FreeCall.bpl

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index f9d9a92e..da75f4f5 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -399,6 +399,29 @@ Execution trace:
 
 Boogie program verifier finished with 1 verified, 4 errors
 
+-------------------- FreeCall.bpl --------------------
+FreeCall.bpl(37,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(8,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    FreeCall.bpl(37,5): anon0
+FreeCall.bpl(42,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(6,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    FreeCall.bpl(42,5): anon0
+FreeCall.bpl(59,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(16,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    FreeCall.bpl(59,5): anon0
+FreeCall.bpl(66,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(14,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    FreeCall.bpl(66,5): anon0
+FreeCall.bpl(87,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    FreeCall.bpl(85,5): anon0
+
+Boogie program verifier finished with 8 verified, 5 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/FreeCall.bpl b/Test/test2/FreeCall.bpl
new file mode 100644
index 00000000..06eb737e
--- /dev/null
+++ b/Test/test2/FreeCall.bpl
@@ -0,0 +1,96 @@
+// Test the implementation of free calls. These calls don't check the preconditions of the
+// called procedure in the caller.
+
+
+procedure Uncallable(i: int)
+  requires 0 <= i;
+  free requires true;
+  requires false;
+{
+
+}
+
+procedure UncallableReturn(i: int) returns (b: bool)
+  requires 0 <= i;
+  free requires true;
+  requires false;
+{
+    b := true;
+}
+
+function T(b: bool) : bool
+{
+    b == true
+}
+
+procedure TestCallForall(b: bool)
+  requires T(b);
+  free requires true;
+  ensures T(b);
+{
+
+}
+
+
+procedure NormalCall0()
+{
+    call Uncallable(0); // error: precondition violation
+}
+
+procedure NormalCall1()
+{
+    call Uncallable(-1); // error: precondition violation
+}
+
+procedure FreeCall0()
+{
+    free call Uncallable(0);
+}
+
+procedure FreeCall1()
+{
+    free call Uncallable(-1);
+}
+
+procedure NormalCall2()
+{
+    var b: bool;
+
+    call b := UncallableReturn(0); // error: precondition violation
+}
+
+procedure NormalCall3()
+{
+    var b: bool;
+
+    call b := UncallableReturn(-1); // error: precondition violation
+}
+
+procedure FreeCall3()
+{
+    var b: bool;
+
+    free call b := UncallableReturn(0);
+}
+
+procedure FreeCall4()
+{
+    var b: bool;
+
+    free call b := UncallableReturn(-1);
+}
+
+procedure NormalCall5()
+{
+    call forall TestCallForall(*);
+    assert T(true);
+    assert T(false); // error
+}
+
+procedure FreeCall5()
+{
+    free call forall TestCallForall(*);
+    assert T(true);
+    assert T(false);
+    assert false;
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index c9d4feac..3dc7d0c3 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 SelectiveChecking.bpl) do (
+            IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl FreeCall.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /noinfer %%f
@@ -24,7 +24,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
 )
 
 echo -------------------- sk_hack.bpl --------------------
-%BGEXE% %* /noinfer /bv:z sk_hack.bpl 
+%BGEXE% %* /noinfer /bv:z sk_hack.bpl
 
 for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
   echo.
-- 
cgit v1.2.3