diff options
| author |  wuestholz <unknown> | 2013-06-10 14:34:54 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-10 14:34:54 -0700 |
| commit | bfa3c64c4a4c583e30242da5a11b37800513418e (patch) | |
| tree | 771a3f7ca5957c689d62ae35add352db2bf6ae47 /Test/snapshots/Answer | |
| parent | 14ec8db388dc3d4db99fc25a6b8f434bba6fccd9 (diff) | |
Worked on improving program snapshot verification.
Diffstat (limited to 'Test/snapshots/Answer')
| -rw-r--r-- | Test/snapshots/Answer | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index a7a6b0be..676f0323 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -1,4 +1,5 @@ --------------------- Snapshots0.bpl --------------------
+
+-------------------- Snapshots0 --------------------
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots0.v0.bpl(41,5): anon0
@@ -27,7 +28,7 @@ Execution trace: Boogie program verifier finished with 2 verified, 1 error
--------------------- Snapshots1.bpl --------------------
+-------------------- Snapshots1 --------------------
Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots1.v0.bpl(13,5): anon0
@@ -45,7 +46,9 @@ Execution trace: Boogie program verifier finished with 1 verified, 1 error
--------------------- Snapshots2.bpl --------------------
+-------------------- Snapshots2 --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
@@ -57,4 +60,12 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
+-------------------- Snapshots3 --------------------
+
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
|