Enable the VCVariety.BlockNested tests as lit tests.

11 files changed, 103 insertions, 27 deletions

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