From 8f2ef8a079ea77caead0a62f5bec8ce34181d907 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sun, 19 Oct 2014 18:00:27 +0200 Subject: Worked on the verification result caching. --- Test/snapshots/Snapshots25.v0.bpl | 14 ++++++++ Test/snapshots/Snapshots25.v1.bpl | 14 ++++++++ Test/snapshots/Snapshots26.v0.bpl | 14 ++++++++ Test/snapshots/Snapshots26.v1.bpl | 15 +++++++++ Test/snapshots/Snapshots27.v0.bpl | 14 ++++++++ Test/snapshots/Snapshots27.v1.bpl | 16 +++++++++ Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 60 +++++++++++++++++++++++++++++----- 8 files changed, 139 insertions(+), 10 deletions(-) create mode 100644 Test/snapshots/Snapshots25.v0.bpl create mode 100644 Test/snapshots/Snapshots25.v1.bpl create mode 100644 Test/snapshots/Snapshots26.v0.bpl create mode 100644 Test/snapshots/Snapshots26.v1.bpl create mode 100644 Test/snapshots/Snapshots27.v0.bpl create mode 100644 Test/snapshots/Snapshots27.v1.bpl (limited to 'Test/snapshots') diff --git a/Test/snapshots/Snapshots25.v0.bpl b/Test/snapshots/Snapshots25.v0.bpl new file mode 100644 index 00000000..5276f1dd --- /dev/null +++ b/Test/snapshots/Snapshots25.v0.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "0"} M(); + +implementation {:id "M"} {:checksum "1"} M() +{ + var x: int; + + while (*) + { + x := 0; + } + + assert 0 == 0; + assert x != x; +} diff --git a/Test/snapshots/Snapshots25.v1.bpl b/Test/snapshots/Snapshots25.v1.bpl new file mode 100644 index 00000000..fb735930 --- /dev/null +++ b/Test/snapshots/Snapshots25.v1.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "0"} M(); + +implementation {:id "M"} {:checksum "2"} M() +{ + var x: int; + + while (*) + { + x := 1; + } + + assert 0 == 0; + assert x != x; +} diff --git a/Test/snapshots/Snapshots26.v0.bpl b/Test/snapshots/Snapshots26.v0.bpl new file mode 100644 index 00000000..5276f1dd --- /dev/null +++ b/Test/snapshots/Snapshots26.v0.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "0"} M(); + +implementation {:id "M"} {:checksum "1"} M() +{ + var x: int; + + while (*) + { + x := 0; + } + + assert 0 == 0; + assert x != x; +} diff --git a/Test/snapshots/Snapshots26.v1.bpl b/Test/snapshots/Snapshots26.v1.bpl new file mode 100644 index 00000000..7c2e3292 --- /dev/null +++ b/Test/snapshots/Snapshots26.v1.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M(); + +implementation {:id "M"} {:checksum "2"} M() +{ + var x: int; + + while (*) + { + x := 0; + x := x + 1; + } + + assert 0 == 0; + assert x != x; +} diff --git a/Test/snapshots/Snapshots27.v0.bpl b/Test/snapshots/Snapshots27.v0.bpl new file mode 100644 index 00000000..5276f1dd --- /dev/null +++ b/Test/snapshots/Snapshots27.v0.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "0"} M(); + +implementation {:id "M"} {:checksum "1"} M() +{ + var x: int; + + while (*) + { + x := 0; + } + + assert 0 == 0; + assert x != x; +} diff --git a/Test/snapshots/Snapshots27.v1.bpl b/Test/snapshots/Snapshots27.v1.bpl new file mode 100644 index 00000000..4d60e149 --- /dev/null +++ b/Test/snapshots/Snapshots27.v1.bpl @@ -0,0 +1,16 @@ +procedure {:checksum "0"} M(); + +implementation {:id "M"} {:checksum "2"} M() +{ + var x: int; + var y: int; + + while (*) + { + x := 0; + y := 0; + } + + assert 0 == 0; + assert x != x; +} diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index d5907196..2924b15a 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately 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 > "%t" +// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately 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 > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index f8b36963..bc847ebe 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -296,11 +296,11 @@ Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)) >>> added after: a##post##2 := a##post##2 && false; Processing command (at Snapshots17.v1.bpl(28,5)) assert true /* checksum: 17-6D-05-FB-27-8E-09-CB-76-67-1B-D1-AC-28-1E-BC */ ; >>> turned assertion into assume statement -Processing command (at Snapshots17.v1.bpl(25,9)) assert false /* checksum: 80-58-47-CB-BE-BA-FC-22-49-6B-79-1F-00-B0-76-C8 */ ; +Processing command (at Snapshots17.v1.bpl(25,9)) assert false /* checksum: BD-BA-41-4E-2B-2F-D9-9F-50-DD-54-70-B0-DE-5B-39 */ ; >>> did nothing -Processing command (at Snapshots17.v1.bpl(12,13)) assert true /* checksum: 8C-AC-68-E0-D9-25-3C-E2-A1-47-07-CD-ED-9B-B8-8A */ ; +Processing command (at Snapshots17.v1.bpl(12,13)) assert true /* checksum: 1F-12-2A-83-92-12-7B-F9-9A-F1-94-FC-3D-F5-37-95 */ ; >>> did nothing -Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1 /* checksum: B4-68-64-D5-1B-10-5F-E3-FA-C7-B8-F7-D1-C5-45-2C */ ; +Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1 /* checksum: 67-12-2A-C6-D4-FB-58-80-9D-35-EF-42-01-EF-4A-7B */ ; >>> did nothing Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold. Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold. @@ -318,12 +318,12 @@ Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)): >>> added after: a##post##0 := a##post##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; -Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0 /* checksum: EB-9A-F3-AB-2C-6D-D5-85-C7-CA-03-01-F2-ED-12-D6 */ ; - >>> did nothing -Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1 /* checksum: DA-9B-89-CB-B7-20-E4-60-00-D9-C2-64-D5-7A-B2-39 */ ; - >>> did nothing -Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2 /* checksum: A8-A9-15-48-2F-DC-37-54-4D-12-CB-D8-39-07-DB-E6 */ ; - >>> did nothing +Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0 /* checksum: B1-21-7E-D6-6E-15-08-55-9F-FC-DD-C4-73-7C-FE-66 */ ; + >>> turned assertion into assume statement +Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1 /* checksum: 40-C2-E2-EC-B1-48-97-30-58-1B-D0-87-76-8D-5E-C9 */ ; + >>> added assume statement for assertion that has been partially verified under "a##post##0#AT#0 && a##post##1#AT#0" +Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2 /* checksum: 18-79-6F-32-17-AC-69-D4-4D-E2-27-78-5D-13-E3-C6 */ ; + >>> added assume statement for assertion that has been partially verified under "a##post##0#AT#1 && a##post##1#AT#1" Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold. Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold. @@ -459,3 +459,45 @@ Processing command (at Snapshots24.v1.bpl(24,5)) assert {:subsumption 0} 3 == 3 Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ; + >>> did nothing +Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ; + >>> did nothing +Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ; + >>> turned assertion into assume statement +Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ; + >>> recycled error and turned assertion into assume statement +Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ; + >>> did nothing +Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ; + >>> did nothing +Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ; + >>> turned assertion into assume statement +Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ; + >>> recycled error and turned assertion into assume statement +Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ; + >>> did nothing +Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ; + >>> did nothing +Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ; + >>> turned assertion into assume statement +Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ; + >>> recycled error and turned assertion into assume statement +Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3