diff options
author | wuestholz <unknown> | 2014-05-27 11:20:17 +0200 |
---|---|---|
committer | wuestholz <unknown> | 2014-05-27 11:20:17 +0200 |
commit | e0a7d0330df42841c0c18a7439b1d60abf7703c9 (patch) | |
tree | 061c46d6ab537d4dd4aa18e6b24c4c019dd345a1 /Test/snapshots | |
parent | 137f285e5a45d5e4ce3eaa40fc68df7890a3d2d7 (diff) |
Added more tests (snapshots).
Diffstat (limited to 'Test/snapshots')
-rw-r--r-- | Test/snapshots/Answer | 11 | ||||
-rw-r--r-- | Test/snapshots/Snapshots6.v0.bpl | 17 | ||||
-rw-r--r-- | Test/snapshots/Snapshots6.v1.bpl | 17 | ||||
-rw-r--r-- | Test/snapshots/Snapshots7.v0.bpl | 19 | ||||
-rw-r--r-- | Test/snapshots/Snapshots7.v1.bpl | 19 | ||||
-rw-r--r-- | Test/snapshots/runtest.bat | 2 | ||||
-rw-r--r-- | Test/snapshots/runtest.snapshot | 2 | ||||
-rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 173 |
8 files changed, 177 insertions, 83 deletions
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
|