summaryrefslogtreecommitdiff
path: root/Test/snapshots/runtest.snapshot.expect
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-06-05 15:03:09 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-06-05 15:03:09 -0400
commit618f037a466cd4392be6e1f4b20e248d58447456 (patch)
tree3c0b51de79e3537d3e94c8f1cca46f32d9a4b974 /Test/snapshots/runtest.snapshot.expect
parent636108e4c302a24ed658b5f09812010b30e36e95 (diff)
parent41082463d783d6f8d8a5aaf69bf459b57bca6000 (diff)
Merge branch 'dfsg_free'
Diffstat (limited to 'Test/snapshots/runtest.snapshot.expect')
-rw-r--r--Test/snapshots/runtest.snapshot.expect142
1 files changed, 142 insertions, 0 deletions
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 4ef6bd20..393c9330 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -666,3 +666,145 @@ Processing command (at Snapshots37.v1.bpl(8,5)) assert l[0];
Snapshots37.v1.bpl(8,5): Error BP5001: This assertion might not hold.
Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots38.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots38.v0.bpl(8,5)) assert r != 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots38.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(8,5)) assert r != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(9,5)) assert 42 <= r;
+ >>> DoNothingToAssert
+Snapshots38.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots38.v2.bpl(7,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+ >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n != 0 ==> 1 <= call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots38.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(8,5)) assert r != 0;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots38.v2.bpl(9,5)) assert 42 <= r;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots39.v0.bpl(8,5)) assert r != 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(8,5)) assert r != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(9,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+Snapshots39.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots39.v2.bpl(7,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+ >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots39.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(8,5)) assert r != 0;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots39.v2.bpl(9,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots40.v0.bpl(7,5)) assert b;
+ >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(8,5)) assert 0 <= call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(9,5)) assert r != 0;
+ >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots40.v1.bpl(7,5)) assert b;
+ >>> RecycleError
+Processing command (at Snapshots40.v1.bpl(8,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(9,5)) assert r != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(10,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+Snapshots40.v1.bpl(10,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing call to procedure Sum in implementation Foo (at Snapshots40.v2.bpl(8,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+ >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots40.v2.bpl(7,5)) assert b;
+ >>> RecycleError
+Processing command (at Snapshots40.v2.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(8,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(9,5)) assert r != 0;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots40.v2.bpl(10,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,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