From c8b3dace6ff23f5554423b41c03d87e024ed1147 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 25 Nov 2014 10:52:54 +0100 Subject: Worked on the verification result caching (extracted functions). --- Test/snapshots/runtest.snapshot.expect | 76 ++++++++++++++++++++-------------- 1 file changed, 46 insertions(+), 30 deletions(-) (limited to 'Test/snapshots') diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 7f912427..c0aced32 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -66,8 +66,9 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)): - >>> added before precondition check: assume {:precondition_previous_snapshot} F0(); -Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} F0(); + >>> added axiom: ##extracted_function##1() == F0() + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(); +Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(); >>> MarkAsFullyVerified Processing command (at Snapshots2.v5.bpl(7,5)) assert F0(); >>> MarkAsFullyVerified @@ -112,9 +113,10 @@ Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)): + >>> added axiom: (forall y##old##0: int :: { ##extracted_function##1(y##old##0) } ##extracted_function##1(y##old##0) == (y##old##0 == y)) >>> added before: y##old##0 := y; - >>> added after: a##post##0 := a##post##0 && y##old##0 == y; -Processing command (at ) a##post##0 := a##post##0 && y##old##0 == y; + >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0); +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0; >>> MarkAsPartiallyVerified @@ -126,9 +128,10 @@ Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)): + >>> added axiom: ##extracted_function##1() == (y < z) >>> added before: y##old##0 := y; - >>> added after: a##post##0 := a##post##0 && y < z; -Processing command (at ) a##post##0 := a##post##0 && y < z; + >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(); +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0; >>> MarkAsPartiallyVerified @@ -141,13 +144,15 @@ Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)): - >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; - >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r; -Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; + >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n)) + >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); +Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); >>> MarkAsFullyVerified Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n; >>> MarkAsFullyVerified -Processing command (at ) a##post##0 := a##post##0 && 0 < call1formal#AT#r; +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x; >>> MarkAsPartiallyVerified @@ -162,13 +167,15 @@ Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)): - >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n && true; - >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r && true; -Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n && true; + >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true)) + >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); +Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); >>> MarkAsFullyVerified Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n; >>> MarkAsFullyVerified -Processing command (at ) a##post##0 := a##post##0 && 0 < call1formal#AT#r && true; +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x; >>> MarkAsPartiallyVerified @@ -181,13 +188,15 @@ Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)): - >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; - >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r; -Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; + >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n)) + >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); +Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); >>> MarkAsFullyVerified Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n; >>> MarkAsFullyVerified -Processing command (at ) a##post##0 := a##post##0 && 0 < call1formal#AT#r; +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x; >>> MarkAsPartiallyVerified @@ -202,9 +211,11 @@ Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might Boogie program verifier finished with 0 verified, 1 error Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)): - >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; - >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r; -Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; + >>> added axiom: (forall call0formal#AT#n: int :: { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n)) + >>> added axiom: (forall call1formal#AT#r: int :: { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r)) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); + >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r); +Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n); >>> DropAssume Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n; >>> RecycleError @@ -241,8 +252,9 @@ Processing command (at Snapshots14.v0.bpl(7,5)) assert false; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)): - >>> added after: a##post##0 := a##post##0 && F() && G(); -Processing command (at ) a##post##0 := a##post##0 && F() && G(); + >>> added axiom: ##extracted_function##1() == (F() && G()) + >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(); +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots14.v1.bpl(7,5)) assert false; >>> MarkAsPartiallyVerified @@ -337,8 +349,9 @@ Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)): - >>> added before precondition check: assume {:precondition_previous_snapshot} 2 == 2; -Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} 2 == 2; + >>> added axiom: ##extracted_function##1() == (2 == 2) + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(); +Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(); >>> MarkAsFullyVerified Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2; >>> MarkAsFullyVerified @@ -357,7 +370,8 @@ Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)): - >>> added after: a##post##0 := a##post##0 && 0 != 0; + >>> added axiom: ##extracted_function##1() == (0 != 0) + >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(); Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1; >>> MarkAsPartiallyVerified Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2; @@ -552,8 +566,9 @@ Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)): - >>> added after: a##post##0 := a##post##0 && call0old#AT#g < g; -Processing command (at ) a##post##0 := a##post##0 && call0old#AT#g < g; + >>> added axiom: (forall call0old#AT#g: int :: { ##extracted_function##1(call0old#AT#g) } ##extracted_function##1(call0old#AT#g) == (call0old#AT#g < g)) + >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g); +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g; >>> MarkAsPartiallyVerified @@ -565,9 +580,10 @@ Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)): + >>> added axiom: (forall g##old##0: int :: { ##extracted_function##1(g##old##0) } ##extracted_function##1(g##old##0) == (g##old##0 < g)) >>> added before: g##old##0 := g; - >>> added after: a##post##0 := a##post##0 && g##old##0 < g; -Processing command (at ) a##post##0 := a##post##0 && g##old##0 < g; + >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0); +Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g; >>> MarkAsPartiallyVerified -- cgit v1.2.3