From 5a92b5242c4febbf32371919845eadc22d405fad Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 24 Jan 2015 14:40:01 +0100 Subject: Worked on the verification result caching (use weights for extracted functions). --- Test/snapshots/runtest.snapshot.expect | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'Test/snapshots') diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 5d641f98..8f3c2015 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -113,7 +113,7 @@ 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, y: int :: { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y)) + >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y)) >>> added before: y##old##0 := y; >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y); Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y); @@ -128,7 +128,7 @@ 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: (forall y: int, z: int :: { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z)) + >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z)) >>> added before: y##old##0 := y; >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y, z); Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(y, z); @@ -144,8 +144,8 @@ 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 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 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 call1formal#AT#r: int :: {:weight 30} { ##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); @@ -167,8 +167,8 @@ 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 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 axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true)) + >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##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); @@ -188,8 +188,8 @@ 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 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 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 call1formal#AT#r: int :: {:weight 30} { ##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); @@ -211,8 +211,8 @@ 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 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 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 call1formal#AT#r: int :: {:weight 30} { ##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); @@ -566,7 +566,7 @@ 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 axiom: (forall call0old#AT#g: int, g: int :: { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g)) + >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g)) >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g); Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g); >>> AssumeNegationOfAssumptionVariable @@ -580,7 +580,7 @@ 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, g: int :: { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g)) + >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g)) >>> added before: g##old##0 := g; >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g); Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g); -- cgit v1.2.3