diff options
| author |  Rustan Leino <leino@microsoft.com> | 2015-08-27 20:10:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2015-08-28 13:29:56 -0700 |
| commit | 21f1cfff139759d9b9f91ed800da2158daca8ed4 (patch) | |
| tree | e9665d1ed7561e244372f167fcc6d90abd32127b /Test/snapshots/runtest.snapshot.expect | |
| parent | 8f64d5c104efe69c5d561c1b22c3e1320bba04fa (diff) | |
Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code.
Diffstat (limited to 'Test/snapshots/runtest.snapshot.expect')
| -rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 637dd088..9dd3d0ec 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -648,3 +648,46 @@ Processing command (at Snapshots35.v1.bpl(5,5)) assert p; Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots41.v0.bpl(3,23)) assert x < 20 || 10 <= x;
+ >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(4,3)) assert x < 10;
+ >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(5,3)) assert 0 <= call0formal#AT#y;
+ >>> DoNothingToAssert
+Snapshots41.v0.bpl(4,3): Error BP5001: This assertion might not hold.
+Snapshots41.v0.bpl(5,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v0.bpl(9,3): Related location: This is the precondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(15,3)) assert 2 <= z;
+ >>> DoNothingToAssert
+Snapshots41.v0.bpl(22,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v0.bpl(15,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(28,3)) assert u != 53;
+ >>> DoNothingToAssert
+Snapshots41.v0.bpl(28,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v0.bpl(34,3)) assert true;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 4 errors
+Processing command (at Snapshots41.v1.bpl(4,1)) assert x < 20 || 10 <= x;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots41.v1.bpl(6,8)) assert x < 10;
+ >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(7,3)) assert 0 <= call0formal#AT#y;
+ >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(8,3)) assert x == 7;
+ >>> DoNothingToAssert
+Snapshots41.v1.bpl(6,8): Error BP5001: This assertion might not hold.
+Snapshots41.v1.bpl(7,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v1.bpl(13,10): Related location: This is the precondition that might not hold.
+Snapshots41.v1.bpl(8,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v1.bpl(27,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots41.v1.bpl(21,3)) assert 2 <= z;
+ >>> DoNothingToAssert
+Snapshots41.v1.bpl(29,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v1.bpl(21,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v1.bpl(35,8)) assert u != 53;
+ >>> RecycleError
+Snapshots41.v1.bpl(35,8): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 2 verified, 5 errors
|