From 6d5ddf853694b2b8014585dd1e40cc10efbaddea Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Sun, 17 May 2015 13:06:58 +0200 Subject: Make caching of verification results more fine-grained for changes that affect preconditions. --- Test/snapshots/Snapshots34.v0.bpl | 7 ++ Test/snapshots/Snapshots34.v1.bpl | 6 ++ Test/snapshots/Snapshots35.v0.bpl | 7 ++ Test/snapshots/Snapshots35.v1.bpl | 6 ++ Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 126 +++++++++++++++++++++++---------- 6 files changed, 115 insertions(+), 39 deletions(-) create mode 100644 Test/snapshots/Snapshots34.v0.bpl create mode 100644 Test/snapshots/Snapshots34.v1.bpl create mode 100644 Test/snapshots/Snapshots35.v0.bpl create mode 100644 Test/snapshots/Snapshots35.v1.bpl (limited to 'Test') diff --git a/Test/snapshots/Snapshots34.v0.bpl b/Test/snapshots/Snapshots34.v0.bpl new file mode 100644 index 00000000..e3522645 --- /dev/null +++ b/Test/snapshots/Snapshots34.v0.bpl @@ -0,0 +1,7 @@ +procedure {:checksum "0"} P(); + requires 0 != 0; + +implementation {:id "P"} {:checksum "1"} P() +{ + assert 1 != 1; +} diff --git a/Test/snapshots/Snapshots34.v1.bpl b/Test/snapshots/Snapshots34.v1.bpl new file mode 100644 index 00000000..b374f7c0 --- /dev/null +++ b/Test/snapshots/Snapshots34.v1.bpl @@ -0,0 +1,6 @@ +procedure {:checksum "2"} P(); + +implementation {:id "P"} {:checksum "1"} P() +{ + assert 1 != 1; +} diff --git a/Test/snapshots/Snapshots35.v0.bpl b/Test/snapshots/Snapshots35.v0.bpl new file mode 100644 index 00000000..adfd6a69 --- /dev/null +++ b/Test/snapshots/Snapshots35.v0.bpl @@ -0,0 +1,7 @@ +procedure {:checksum "0"} P(b: bool); + requires b; + +implementation {:id "P"} {:checksum "1"} P(p: bool) +{ + assert p; +} diff --git a/Test/snapshots/Snapshots35.v1.bpl b/Test/snapshots/Snapshots35.v1.bpl new file mode 100644 index 00000000..bec381af --- /dev/null +++ b/Test/snapshots/Snapshots35.v1.bpl @@ -0,0 +1,6 @@ +procedure {:checksum "2"} P(b: bool); + +implementation {:id "P"} {:checksum "1"} P(p: bool) +{ + assert p; +} diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index a203ffac..01a231fe 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl > "%t" +// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 8f3c2015..637dd088 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -40,8 +40,13 @@ Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 1 verified, 1 error Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)): + >>> added after: a##cached##0 := a##cached##0 && true; +Processing implementation P2 (at Snapshots1.v2.bpl(12,51)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true; Processing command (at Snapshots1.v2.bpl(5,5)) assert false; >>> DoNothingToAssert +Processing command (at ) a##cached##0 := a##cached##0 && true; + >>> AssumeNegationOfAssumptionVariable 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. Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2; @@ -52,34 +57,45 @@ Boogie program verifier finished with 1 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P0 (at Snapshots2.v2.bpl(4,51)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true; Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)): + >>> added after: a##cached##1 := a##cached##1 && true; Processing command (at Snapshots2.v2.bpl(6,5)) assert F0(); >>> DoNothingToAssert Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P0 (at Snapshots2.v3.bpl(4,51)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##1 := a##cached##1 && false; Processing command (at Snapshots2.v3.bpl(6,5)) assert F0(); >>> DoNothingToAssert 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)): +Processing implementation P0 (at Snapshots2.v5.bpl(5,51)): >>> 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 + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(); +Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)): + >>> added axiom: ##extracted_function##2() == F0() + >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##2(); + >>> added after: a##cached##1 := a##cached##1 && true; +Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##2(); + >>> MarkAsPartiallyVerified Processing command (at Snapshots2.v5.bpl(7,5)) assert F0(); - >>> MarkAsFullyVerified + >>> MarkAsPartiallyVerified Processing command (at Snapshots2.v5.bpl(3,1)) assert F0(); - >>> MarkAsFullyVerified + >>> MarkAsPartiallyVerified Boogie program verifier finished with 1 verified, 0 errors Processing command (at Snapshots3.v0.bpl(2,1)) assert G(); >>> DoNothingToAssert Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P0 (at Snapshots3.v1.bpl(4,51)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing command (at Snapshots3.v1.bpl(2,1)) assert G(); >>> DoNothingToAssert Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path. @@ -89,7 +105,7 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 3 verified, 0 errors Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##0 := a##cached##0 && false; Processing command (at Snapshots4.v1.bpl(23,5)) assert false; >>> DoNothingToAssert Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold. @@ -103,6 +119,8 @@ Processing command (at Snapshots5.v0.bpl(5,5)) assert false; >>> DoNothingToAssert Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P0 (at Snapshots5.v1.bpl(3,51)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing command (at Snapshots5.v1.bpl(5,5)) assert false; >>> DoNothingToAssert Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold. @@ -115,8 +133,8 @@ 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 :: {: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); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0; >>> MarkAsPartiallyVerified @@ -130,8 +148,8 @@ 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 :: {: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); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y, z); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(y, z); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0; >>> MarkAsPartiallyVerified @@ -147,12 +165,12 @@ Processing call to procedure N in implementation M (at Snapshots8.v1.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 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); + >>> added after: a##cached##0 := a##cached##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 && ##extracted_function##2(call1formal#AT#r); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x; >>> MarkAsPartiallyVerified @@ -170,12 +188,12 @@ Processing call to procedure N in implementation M (at Snapshots9.v1.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 && 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); + >>> added after: a##cached##0 := a##cached##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 && ##extracted_function##2(call1formal#AT#r); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x; >>> MarkAsPartiallyVerified @@ -191,12 +209,12 @@ Processing call to procedure N in implementation M (at Snapshots10.v1.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 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); + >>> added after: a##cached##0 := a##cached##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 && ##extracted_function##2(call1formal#AT#r); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x; >>> MarkAsPartiallyVerified @@ -214,7 +232,7 @@ Processing call to procedure N in implementation M (at Snapshots11.v1.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 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); + >>> added after: a##cached##0 := a##cached##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; @@ -230,7 +248,7 @@ Processing command (at Snapshots12.v0.bpl(7,5)) assert false; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##0 := a##cached##0 && false; Processing command (at Snapshots12.v1.bpl(7,5)) assert false; >>> DoNothingToAssert Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold. @@ -241,7 +259,7 @@ Processing command (at Snapshots13.v0.bpl(7,5)) assert false; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##0 := a##cached##0 && false; Processing command (at Snapshots13.v1.bpl(7,5)) assert false; >>> DoNothingToAssert Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold. @@ -253,8 +271,8 @@ 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 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(); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots14.v1.bpl(7,5)) assert false; >>> MarkAsPartiallyVerified @@ -270,9 +288,9 @@ Processing command (at Snapshots15.v0.bpl(13,5)) assert false; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##0 := a##cached##0 && false; Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)): - >>> added after: a##post##1 := a##post##1 && false; + >>> added after: a##cached##1 := a##cached##1 && false; Processing command (at Snapshots15.v1.bpl(5,5)) assert true; >>> MarkAsFullyVerified Processing command (at Snapshots15.v1.bpl(9,5)) assert true; @@ -302,11 +320,11 @@ Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##0 := a##cached##0 && false; Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)): - >>> added after: a##post##1 := a##post##1 && false; + >>> added after: a##cached##1 := a##cached##1 && false; Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)): - >>> added after: a##post##2 := a##post##2 && false; + >>> added after: a##cached##2 := a##cached##2 && false; Processing command (at Snapshots17.v1.bpl(28,5)) assert true; >>> MarkAsFullyVerified Processing command (at Snapshots17.v1.bpl(25,9)) assert false; @@ -328,9 +346,9 @@ Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2; Boogie program verifier finished with 1 verified, 0 errors Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##0 := a##cached##0 && false; Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)): - >>> added after: a##post##1 := a##post##1 && false; + >>> added after: a##cached##1 := a##cached##1 && false; Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0; >>> MarkAsFullyVerified Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1; @@ -351,13 +369,14 @@ Boogie program verifier finished with 0 verified, 1 error Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)): >>> added axiom: ##extracted_function##1() == (2 == 2) >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(); + >>> added after: a##cached##0 := a##cached##0 && true; 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 Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1; - >>> RecycleError -Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold. + >>> DoNothingToAssert +Snapshots19.v1.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1; @@ -371,7 +390,7 @@ 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 axiom: ##extracted_function##1() == (0 != 0) - >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(); + >>> added after: a##cached##0 := a##cached##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; @@ -567,8 +586,8 @@ 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 :: {: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); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g; >>> MarkAsPartiallyVerified @@ -582,8 +601,8 @@ 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 :: {: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); + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g); >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g; >>> MarkAsPartiallyVerified @@ -594,7 +613,38 @@ Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g; >>> DoNothingToAssert Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P (at Snapshots33.v1.bpl(3,42)): + >>> added axiom: (forall g: int :: {:weight 30} { ##extracted_function##1(g) } ##extracted_function##1(g) == (g == 0)) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(g); Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)): - >>> added after: a##post##0 := a##post##0 && false; + >>> added after: a##cached##1 := a##cached##1 && false; + +Boogie program verifier finished with 1 verified, 0 errors +Processing command (at Snapshots34.v0.bpl(6,5)) assert 1 != 1; + >>> DoNothingToAssert + +Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P (at Snapshots34.v1.bpl(3,42)): + >>> added axiom: ##extracted_function##1() == (0 != 0) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at Snapshots34.v1.bpl(5,5)) assert 1 != 1; + >>> MarkAsPartiallyVerified +Snapshots34.v1.bpl(5,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots35.v0.bpl(6,5)) assert p; + >>> DoNothingToAssert Boogie program verifier finished with 1 verified, 0 errors +Processing implementation P (at Snapshots35.v1.bpl(3,42)): + >>> added axiom: (forall p: bool :: {:weight 30} { ##extracted_function##1(p) } ##extracted_function##1(p) == p) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(p); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(p); + >>> AssumeNegationOfAssumptionVariable +Processing command (at Snapshots35.v1.bpl(5,5)) assert p; + >>> MarkAsPartiallyVerified +Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3