From e0a7d0330df42841c0c18a7439b1d60abf7703c9 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 27 May 2014 11:20:17 +0200 Subject: Added more tests (snapshots). --- Test/snapshots/Answer | 11 +++ Test/snapshots/Snapshots6.v0.bpl | 17 ++++ Test/snapshots/Snapshots6.v1.bpl | 17 ++++ Test/snapshots/Snapshots7.v0.bpl | 19 ++++ Test/snapshots/Snapshots7.v1.bpl | 19 ++++ Test/snapshots/runtest.bat | 2 +- Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 173 ++++++++++++++++++--------------- 8 files changed, 177 insertions(+), 83 deletions(-) create mode 100644 Test/snapshots/Snapshots6.v0.bpl create mode 100644 Test/snapshots/Snapshots6.v1.bpl create mode 100644 Test/snapshots/Snapshots7.v0.bpl create mode 100644 Test/snapshots/Snapshots7.v1.bpl (limited to 'Test/snapshots') diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index 7826d2f0..0ba6f920 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -79,3 +79,14 @@ Execution trace: Snapshots5.v1.bpl(5,5): anon0 Boogie program verifier finished with 0 verified, 1 error + +Boogie program verifier finished with 1 verified, 0 errors +Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots6.v1.bpl(9,7): anon0 + +Boogie program verifier finished with 0 verified, 1 error + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/snapshots/Snapshots6.v0.bpl b/Test/snapshots/Snapshots6.v0.bpl new file mode 100644 index 00000000..157fc45b --- /dev/null +++ b/Test/snapshots/Snapshots6.v0.bpl @@ -0,0 +1,17 @@ +var x: int; +var y: int; + +procedure {:checksum "0"} M(); + modifies x, y; + +implementation {:checksum "1"} M() +{ + y := 0; + + call N(); + + assert y == 0; +} + +procedure {:checksum "2"} N(); + modifies x; diff --git a/Test/snapshots/Snapshots6.v1.bpl b/Test/snapshots/Snapshots6.v1.bpl new file mode 100644 index 00000000..eb139546 --- /dev/null +++ b/Test/snapshots/Snapshots6.v1.bpl @@ -0,0 +1,17 @@ +var x: int; +var y: int; + +procedure {:checksum "0"} M(); + modifies x, y; + +implementation {:checksum "1"} M() +{ + y := 0; + + call N(); + + assert y == 0; +} + +procedure {:checksum "3"} N(); + modifies x, y; diff --git a/Test/snapshots/Snapshots7.v0.bpl b/Test/snapshots/Snapshots7.v0.bpl new file mode 100644 index 00000000..6b99de1b --- /dev/null +++ b/Test/snapshots/Snapshots7.v0.bpl @@ -0,0 +1,19 @@ +var x: int; +var y: int; +var z: int; + +procedure {:checksum "0"} M(); + modifies x, y, z; + +implementation {:checksum "1"} M() +{ + z := 0; + + call N(); + + assert y < 0; +} + +procedure {:checksum "2"} N(); + modifies x, y; + ensures y < z; diff --git a/Test/snapshots/Snapshots7.v1.bpl b/Test/snapshots/Snapshots7.v1.bpl new file mode 100644 index 00000000..bba0978b --- /dev/null +++ b/Test/snapshots/Snapshots7.v1.bpl @@ -0,0 +1,19 @@ +var x: int; +var y: int; +var z: int; + +procedure {:checksum "0"} M(); + modifies x, y, z; + +implementation {:checksum "1"} M() +{ + z := 0; + + call N(); + + assert y < 0; +} + +procedure {:checksum "3"} N(); + modifies x; + ensures y < z; diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat index b7cb641a..7821e39c 100644 --- a/Test/snapshots/runtest.bat +++ b/Test/snapshots/runtest.bat @@ -4,5 +4,5 @@ setlocal set BOOGIEDIR=..\..\Binaries set BGEXE=%BOOGIEDIR%\Boogie.exe -%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl +%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index 6edd51ac..fe5c1b23 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl > %t +// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl > %t // RUN: %diff %s.expect %t diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 3c984793..0ba6f920 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -1,81 +1,92 @@ -Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v0.bpl(41,5): anon0 -Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v0.bpl(8,5): anon0 -Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v0.bpl(19,5): anon0 -Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v0.bpl(30,5): anon0 - -Boogie program verifier finished with 0 verified, 4 errors -Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v0.bpl(41,5): anon0 -Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v1.bpl(30,5): anon0 - -Boogie program verifier finished with 2 verified, 2 errors -Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots0.v0.bpl(41,5): anon0 - -Boogie program verifier finished with 2 verified, 1 error -Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots1.v0.bpl(13,5): anon0 - -Boogie program verifier finished with 1 verified, 1 error -Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots1.v1.bpl(13,5): anon0 - -Boogie program verifier finished with 1 verified, 1 error -Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold. -Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold. -Execution trace: - Snapshots1.v2.bpl(5,5): anon0 - -Boogie program verifier finished with 1 verified, 1 error - -Boogie program verifier finished with 1 verified, 0 errors - -Boogie program verifier finished with 1 verified, 0 errors - -Boogie program verifier finished with 1 verified, 0 errors - -Boogie program verifier finished with 1 verified, 0 errors - -Boogie program verifier finished with 1 verified, 0 errors - -Boogie program verifier finished with 1 verified, 0 errors - -Boogie program verifier finished with 1 verified, 0 errors -Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path. -Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold. -Execution trace: - Snapshots3.v1.bpl(6,1): anon0 - -Boogie program verifier finished with 0 verified, 1 error - -Boogie program verifier finished with 3 verified, 0 errors -Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots4.v1.bpl(23,5): anon0 -Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path. -Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold. -Execution trace: - Snapshots4.v1.bpl(33,1): anon0 - -Boogie program verifier finished with 2 verified, 2 errors - -Boogie program verifier finished with 1 verified, 0 errors -Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold. -Execution trace: - Snapshots5.v1.bpl(5,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error +Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v0.bpl(41,5): anon0 +Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v0.bpl(8,5): anon0 +Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v0.bpl(19,5): anon0 +Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v0.bpl(30,5): anon0 + +Boogie program verifier finished with 0 verified, 4 errors +Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v0.bpl(41,5): anon0 +Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v1.bpl(30,5): anon0 + +Boogie program verifier finished with 2 verified, 2 errors +Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots0.v0.bpl(41,5): anon0 + +Boogie program verifier finished with 2 verified, 1 error +Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots1.v0.bpl(13,5): anon0 + +Boogie program verifier finished with 1 verified, 1 error +Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots1.v1.bpl(13,5): anon0 + +Boogie program verifier finished with 1 verified, 1 error +Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold. +Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold. +Execution trace: + Snapshots1.v2.bpl(5,5): anon0 + +Boogie program verifier finished with 1 verified, 1 error + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors +Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path. +Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold. +Execution trace: + Snapshots3.v1.bpl(6,1): anon0 + +Boogie program verifier finished with 0 verified, 1 error + +Boogie program verifier finished with 3 verified, 0 errors +Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots4.v1.bpl(23,5): anon0 +Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path. +Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold. +Execution trace: + Snapshots4.v1.bpl(33,1): anon0 + +Boogie program verifier finished with 2 verified, 2 errors + +Boogie program verifier finished with 1 verified, 0 errors +Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots5.v1.bpl(5,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error + +Boogie program verifier finished with 1 verified, 0 errors +Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Snapshots6.v1.bpl(9,7): anon0 + +Boogie program verifier finished with 0 verified, 1 error + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors -- cgit v1.2.3