diff options
| author |  wuestholz <unknown> | 2011-09-14 16:28:25 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-09-14 16:28:25 +0200 |
| commit | c250f55e7af88a3671262e2c0522664f299ef2f2 (patch) | |
| tree | 26755b6bff316c4d656d70cf69dc6ca6bdfbe589 /Test/test2 | |
| parent | 23a94e0bbd32c8c612cb79a6745b5bee4dd667dd (diff) | |
Added "free call" statements that don't check the precondition in the caller.
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 23 | ||||
| -rw-r--r-- | Test/test2/FreeCall.bpl | 96 | ||||
| -rw-r--r-- | Test/test2/runtest.bat | 4 |
3 files changed, 121 insertions, 2 deletions
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.
|