diff options
Diffstat (limited to 'Test/test2')
-rw-r--r-- | Test/test2/Answer | 33 | ||||
-rw-r--r-- | Test/test2/CallForall.bpl | 134 | ||||
-rw-r--r-- | Test/test2/FreeCall.bpl | 14 | ||||
-rw-r--r-- | Test/test2/runtest.bat | 2 |
4 files changed, 2 insertions, 181 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index 9625c4db..4a7fd32f 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -424,11 +424,8 @@ 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
+Boogie program verifier finished with 7 verified, 4 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
@@ -462,34 +459,6 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
--------------------- CallForall.bpl --------------------
-CallForall.bpl(17,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(17,3): anon0
-CallForall.bpl(29,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(28,3): anon0
-CallForall.bpl(41,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(40,3): anon0
-CallForall.bpl(47,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(46,3): anon0
-CallForall.bpl(75,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(75,3): anon0
-CallForall.bpl(111,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(109,3): anon0
-CallForall.bpl(118,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(117,3): anon0
-CallForall.bpl(125,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(124,3): anon0
-
-Boogie program verifier finished with 10 verified, 8 errors
-
-------------------- ContractEvaluationOrder.bpl --------------------
ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path.
ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
diff --git a/Test/test2/CallForall.bpl b/Test/test2/CallForall.bpl deleted file mode 100644 index 98a62103..00000000 --- a/Test/test2/CallForall.bpl +++ /dev/null @@ -1,134 +0,0 @@ -function G(int) returns (int);
-axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x);
-
-function F(int) returns (int);
-axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5);
-
-procedure Lemma(y: int)
- requires 0 <= y;
- ensures F(y) == 5;
-{
- // proof:
- assert G(y) == y;
-}
-
-procedure Main0()
-{
- assert F(2) == 5; // error: cannot prove this directly, because of the trigger
-}
-
-procedure Main1()
-{
- call Lemma(2);
- assert F(2) == 5;
-}
-
-procedure Main2()
-{
- call Lemma(3);
- assert F(2) == 5; // error: Lemma was instantiated the wrong way
-}
-
-procedure Main3()
-{
- call forall Lemma(*);
- assert F(2) == 5;
-}
-
-procedure Main4()
-{
- call forall Lemma(*);
- assert false; // error
-}
-
-procedure Main5(z: int)
-{
- call forall Lemma(*);
- assert F(z) == 5; // error: z might be negative
-}
-
-procedure Main6(z: int)
- requires 0 <= z;
-{
- call forall Lemma(*);
- assert F(z) == 5;
-}
-
-// ------------ several parameters
-
-function K(int, int) returns (int);
-axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25);
-
-procedure MultivarLemma(x: int, y: int)
- requires 0 <= x;
- requires 0 <= y;
- ensures K(x,y) == 25;
-{
- // proof:
- assert G(x) == x;
- assert G(y) == y;
-}
-
-procedure Multi0(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- assert K(x,y) == 25; // error
-}
-
-procedure Multi1(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call MultivarLemma(x, y);
- assert K(x,y) == 25;
-}
-
-procedure Multi2(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(x, y);
- assert K(x,y) == 25;
-}
-
-procedure Multi3(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(*, y);
- assert K(x,y) == 25;
-}
-
-procedure Multi4(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(x, *);
- assert K(x,y) == 25;
-}
-
-procedure Multi5(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(2 + 100, *);
- assert K(102, y) == 25;
- assert false; // error
-}
-
-procedure Multi6(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(*, y);
- assert K(x+2,y+2) == 25; // error
-}
-
-procedure Multi7(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(x, *);
- assert K(x+2,y+2) == 25; // error
-}
-
-procedure Multi8(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(*, *);
- assert K(x+2,y+2) == 25; // that's the ticket!
-}
-
diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl index 06eb737e..a873a4e6 100644 --- a/Test/test2/FreeCall.bpl +++ b/Test/test2/FreeCall.bpl @@ -80,17 +80,3 @@ procedure FreeCall4() 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 f32bf844..89715252 100644 --- a/Test/test2/runtest.bat +++ b/Test/test2/runtest.bat @@ -27,7 +27,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do ( echo -------------------- sk_hack.bpl --------------------
%BGEXE% %* /noinfer sk_hack.bpl
-for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
+for %%f in (ContractEvaluationOrder.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* %%f
|