diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/snapshots/Snapshots21.v0.bpl | 15 | ||||
-rw-r--r-- | Test/snapshots/Snapshots21.v1.bpl | 15 | ||||
-rw-r--r-- | Test/snapshots/runtest.snapshot | 2 | ||||
-rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 21 |
4 files changed, 52 insertions, 1 deletions
diff --git a/Test/snapshots/Snapshots21.v0.bpl b/Test/snapshots/Snapshots21.v0.bpl new file mode 100644 index 00000000..4a4080f5 --- /dev/null +++ b/Test/snapshots/Snapshots21.v0.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+ if (*)
+ {
+ assert 1 != 1; // error
+ }
+ else
+ {
+ assert 2 != 2; // error
+ }
+
+ assert 3 != 3;
+}
diff --git a/Test/snapshots/Snapshots21.v1.bpl b/Test/snapshots/Snapshots21.v1.bpl new file mode 100644 index 00000000..ef51e5ac --- /dev/null +++ b/Test/snapshots/Snapshots21.v1.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+ if (*)
+ {
+ assert 1 == 1;
+ }
+ else
+ {
+ assert 2 != 2; // error
+ }
+
+ assert 3 != 3; // error
+}
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index 57ca7f5a..e73e4eba 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl > "%t" +// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 7b9241d8..daabfca9 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -206,3 +206,24 @@ Execution trace: Snapshots20.v1.bpl(13,9): anon4_Else
Boogie program verifier finished with 0 verified, 2 errors
+Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots21.v0.bpl(5,5): anon0
+ Snapshots21.v0.bpl(7,9): anon4_Then
+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots21.v0.bpl(5,5): anon0
+ Snapshots21.v0.bpl(11,9): anon4_Else
+
+Boogie program verifier finished with 0 verified, 2 errors
+Snapshots21.v1.bpl(11,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots21.v1.bpl(5,5): anon0
+ Snapshots21.v1.bpl(11,9): anon4_Else
+Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots21.v1.bpl(5,5): anon0
+ Snapshots21.v1.bpl(7,9): anon4_Then
+ Snapshots21.v1.bpl(14,5): anon3
+
+Boogie program verifier finished with 0 verified, 2 errors
|