From eb766c19e8e082cc2164859c19c3a7e27feef84b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 16:50:59 +0100 Subject: Enable the VCVariety.BlockNested tests as lit tests. --- Test/test7/Answer | 54 +++++++++++++------------- Test/test7/MultipleErrors.bpl | 21 ++++++++++ Test/test7/MultipleErrors.bpl.e1.block.expect | 6 +++ Test/test7/MultipleErrors.bpl.e1.dag.expect | 6 +++ Test/test7/MultipleErrors.bpl.e1.local.expect | 5 +++ Test/test7/MultipleErrors.bpl.e10.dag.expect | 15 +++++++ Test/test7/MultipleErrors.bpl.e10.local.expect | 11 ++++++ Test/test7/NestedVC.bpl | 2 + Test/test7/NestedVC.bpl.expect | 6 +++ Test/test7/UnreachableBlocks.bpl | 2 + Test/test7/UnreachableBlocks.bpl.expect | 2 + 11 files changed, 103 insertions(+), 27 deletions(-) create mode 100644 Test/test7/MultipleErrors.bpl.e1.block.expect create mode 100644 Test/test7/MultipleErrors.bpl.e1.dag.expect create mode 100644 Test/test7/MultipleErrors.bpl.e1.local.expect create mode 100644 Test/test7/MultipleErrors.bpl.e10.dag.expect create mode 100644 Test/test7/MultipleErrors.bpl.e10.local.expect create mode 100644 Test/test7/NestedVC.bpl.expect create mode 100644 Test/test7/UnreachableBlocks.bpl.expect (limited to 'Test/test7') diff --git a/Test/test7/Answer b/Test/test7/Answer index 82c84446..00b9069f 100644 --- a/Test/test7/Answer +++ b/Test/test7/Answer @@ -1,8 +1,8 @@ ------------------------------ NestedVC.bpl --------------------- -NestedVC.bpl(15,4): Error BP5001: This assertion might not hold. +NestedVC.bpl(17,4): Error BP5001: This assertion might not hold. Execution trace: - NestedVC.bpl(14,1): A - NestedVC.bpl(15,1): B + NestedVC.bpl(16,1): A + NestedVC.bpl(17,1): B Boogie program verifier finished with 1 verified, 1 error ------------------------------ UnreachableBlocks.bpl --------------------- @@ -11,54 +11,54 @@ Boogie program verifier finished with 4 verified, 0 errors ------------------------------ MultipleErrors.bpl --------------------- ----- /vc:block -MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(3,1): start - MultipleErrors.bpl(6,1): A + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A Boogie program verifier finished with 0 verified, 1 error ----- /vc:local -MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(10,1): B + MultipleErrors.bpl(31,1): B Boogie program verifier finished with 0 verified, 1 error ----- /vc:dag -MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(3,1): start - MultipleErrors.bpl(6,1): A + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A Boogie program verifier finished with 0 verified, 1 error ----- /errorLimit:10 /vc:local -MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(6,1): A -MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold. + MultipleErrors.bpl(27,1): A +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(10,1): B -MultipleErrors.bpl(15,3): Error BP5001: This assertion might not hold. + MultipleErrors.bpl(31,1): B +MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(14,1): C + MultipleErrors.bpl(35,1): C Boogie program verifier finished with 0 verified, 3 errors ----- /errorLimit:10 /vc:dag -MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(3,1): start - MultipleErrors.bpl(6,1): A -MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold. + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(3,1): start - MultipleErrors.bpl(10,1): B -MultipleErrors.bpl(15,3): Error BP5001: This assertion might not hold. + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(31,1): B +MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(3,1): start - MultipleErrors.bpl(6,1): A - MultipleErrors.bpl(14,1): C + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A + MultipleErrors.bpl(35,1): C Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test7/MultipleErrors.bpl b/Test/test7/MultipleErrors.bpl index 5a2024d4..ac1f7e54 100644 --- a/Test/test7/MultipleErrors.bpl +++ b/Test/test7/MultipleErrors.bpl @@ -1,3 +1,24 @@ +// RUN: %boogie -vc:block -errorLimit:1 -errorTrace:1 -logPrefix:-1block %s > %t1 +// RUN: %diff %s.e1.block.expect %t1 +// RUN: %boogie -vc:local -errorLimit:1 -errorTrace:1 -logPrefix:-1local %s > %t2 +// RUN: %diff %s.e1.local.expect %t2 +// RUN: %boogie -vc:dag -errorLimit:1 -errorTrace:1 -logPrefix:-1dag %s > %t3 +// RUN: %diff %s.e1.dag.expect %t3 +// RUN: %boogie -vc:local -errorLimit:10 -errorTrace:1 -logPrefix:-10local %s > %t4 +// RUN: %diff %s.e10.local.expect %t4 +// RUN: %boogie -vc:dag -errorLimit:10 -errorTrace:1 -logPrefix:-10dag %s > %t5 +// RUN: %diff %s.e10.dag.expect %t5 + +// Author of this comment: mikebarnett ec02177eefb5 +// The following tests are rather fickle at the moment--different errors +// may be reported during different runs. Moreover, it is conceivable that +// the error trace would be reported in different orders, since we do not +// attempt to sort the trace labels at this time. +// An interesting thing is that /vc:local can with Simplify report more than one +// error for this file, even with /errorLimit:1. Other than that, only +// local and dag produce VCs to which Simplify actually produces different +// counterexamples. + procedure P(x: int) { start: diff --git a/Test/test7/MultipleErrors.bpl.e1.block.expect b/Test/test7/MultipleErrors.bpl.e1.block.expect new file mode 100644 index 00000000..73db2a21 --- /dev/null +++ b/Test/test7/MultipleErrors.bpl.e1.block.expect @@ -0,0 +1,6 @@ +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e1.dag.expect b/Test/test7/MultipleErrors.bpl.e1.dag.expect new file mode 100644 index 00000000..73db2a21 --- /dev/null +++ b/Test/test7/MultipleErrors.bpl.e1.dag.expect @@ -0,0 +1,6 @@ +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e1.local.expect b/Test/test7/MultipleErrors.bpl.e1.local.expect new file mode 100644 index 00000000..f4acb100 --- /dev/null +++ b/Test/test7/MultipleErrors.bpl.e1.local.expect @@ -0,0 +1,5 @@ +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(31,1): B + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e10.dag.expect b/Test/test7/MultipleErrors.bpl.e10.dag.expect new file mode 100644 index 00000000..5ac162df --- /dev/null +++ b/Test/test7/MultipleErrors.bpl.e10.dag.expect @@ -0,0 +1,15 @@ +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(31,1): B +MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(24,1): start + MultipleErrors.bpl(27,1): A + MultipleErrors.bpl(35,1): C + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test7/MultipleErrors.bpl.e10.local.expect b/Test/test7/MultipleErrors.bpl.e10.local.expect new file mode 100644 index 00000000..9b685ee3 --- /dev/null +++ b/Test/test7/MultipleErrors.bpl.e10.local.expect @@ -0,0 +1,11 @@ +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(27,1): A +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(31,1): B +MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + MultipleErrors.bpl(35,1): C + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test7/NestedVC.bpl b/Test/test7/NestedVC.bpl index d88eefea..be4e0483 100644 --- a/Test/test7/NestedVC.bpl +++ b/Test/test7/NestedVC.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -vc:nested %s > %t +// RUN: %diff %s.expect %t procedure P() { A: goto B, C; diff --git a/Test/test7/NestedVC.bpl.expect b/Test/test7/NestedVC.bpl.expect new file mode 100644 index 00000000..cf9443b6 --- /dev/null +++ b/Test/test7/NestedVC.bpl.expect @@ -0,0 +1,6 @@ +NestedVC.bpl(17,4): Error BP5001: This assertion might not hold. +Execution trace: + NestedVC.bpl(16,1): A + NestedVC.bpl(17,1): B + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test7/UnreachableBlocks.bpl b/Test/test7/UnreachableBlocks.bpl index 6ed287a3..fd31ebe9 100644 --- a/Test/test7/UnreachableBlocks.bpl +++ b/Test/test7/UnreachableBlocks.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -vc:nested %s > %t +// RUN: %diff %s.expect %t // In the following program, block "A" has no dominator, which would cause Boogie // to crash if Boogie didn't first remove unreachable blocks. That is essentially // what this test tests diff --git a/Test/test7/UnreachableBlocks.bpl.expect b/Test/test7/UnreachableBlocks.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/test7/UnreachableBlocks.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors -- cgit v1.2.3