diff options
Diffstat (limited to 'Test/snapshots/Answer')
| -rw-r--r-- | Test/snapshots/Answer | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index 434cdfda..676f0323 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -1,3 +1,5 @@ +
+-------------------- Snapshots0 --------------------
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots0.v0.bpl(41,5): anon0
@@ -25,3 +27,45 @@ Execution trace: Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- Snapshots1 --------------------
+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
+
+-------------------- Snapshots2 --------------------
+
+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 --------------------
+
+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
|