Initial set of files.

6 files changed, 240 insertions, 0 deletions

diff --git a/Test/test7/Answer b/Test/test7/Answer
new file mode 100644
index 00000000..82c84446
--- /dev/null
+++ b/Test/test7/Answer
@@ -0,0 +1,64 @@
+------------------------------ NestedVC.bpl ---------------------

+NestedVC.bpl(15,4): Error BP5001: This assertion might not hold.

+Execution trace:

+    NestedVC.bpl(14,1): A

+    NestedVC.bpl(15,1): B

+

+Boogie program verifier finished with 1 verified, 1 error

+------------------------------ UnreachableBlocks.bpl ---------------------

+

+Boogie program verifier finished with 4 verified, 0 errors

+------------------------------ MultipleErrors.bpl ---------------------

+

+----- /vc:block

+MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,1): A

+

+Boogie program verifier finished with 0 verified, 1 error

+

+----- /vc:local

+MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    MultipleErrors.bpl(10,1): B

+

+Boogie program verifier finished with 0 verified, 1 error

+

+----- /vc:dag

+MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,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.

+Execution trace:

+    MultipleErrors.bpl(6,1): A

+MultipleErrors.bpl(11,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.

+Execution trace:

+    MultipleErrors.bpl(14,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.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,1): A

+MultipleErrors.bpl(11,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.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,1): A

+    MultipleErrors.bpl(14,1): C

+

+Boogie program verifier finished with 0 verified, 3 errors

diff --git a/Test/test7/MultipleErrors.bpl b/Test/test7/MultipleErrors.bpl
new file mode 100644
index 00000000..5a2024d4
--- /dev/null
+++ b/Test/test7/MultipleErrors.bpl
@@ -0,0 +1,17 @@
+procedure P(x: int)

+{

+start:

+  goto A, B;

+

+A:

+  assert 0 <= x;

+  goto C;

+

+B:

+  assert x < 100;

+  goto C;

+

+C:

+  assert x == 87;

+  return;

+}

diff --git a/Test/test7/NestedVC.bpl b/Test/test7/NestedVC.bpl
new file mode 100644
index 00000000..d88eefea
--- /dev/null
+++ b/Test/test7/NestedVC.bpl
@@ -0,0 +1,21 @@
+procedure P()

+{

+A: goto B, C;

+B: goto G;

+C: goto D, E;

+D: goto F;

+E: goto F;

+F: goto G;

+G: return;

+}

+

+procedure Q(x: bool)

+{

+A: goto B, C;

+B: assert x; goto G;

+C: goto D, E;

+D: goto F;

+E: goto F;

+F: goto G;

+G: return;

+}

diff --git a/Test/test7/Output b/Test/test7/Output
new file mode 100644
index 00000000..82c84446
--- /dev/null
+++ b/Test/test7/Output
@@ -0,0 +1,64 @@
+------------------------------ NestedVC.bpl ---------------------

+NestedVC.bpl(15,4): Error BP5001: This assertion might not hold.

+Execution trace:

+    NestedVC.bpl(14,1): A

+    NestedVC.bpl(15,1): B

+

+Boogie program verifier finished with 1 verified, 1 error

+------------------------------ UnreachableBlocks.bpl ---------------------

+

+Boogie program verifier finished with 4 verified, 0 errors

+------------------------------ MultipleErrors.bpl ---------------------

+

+----- /vc:block

+MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,1): A

+

+Boogie program verifier finished with 0 verified, 1 error

+

+----- /vc:local

+MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    MultipleErrors.bpl(10,1): B

+

+Boogie program verifier finished with 0 verified, 1 error

+

+----- /vc:dag

+MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,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.

+Execution trace:

+    MultipleErrors.bpl(6,1): A

+MultipleErrors.bpl(11,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.

+Execution trace:

+    MultipleErrors.bpl(14,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.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,1): A

+MultipleErrors.bpl(11,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.

+Execution trace:

+    MultipleErrors.bpl(3,1): start

+    MultipleErrors.bpl(6,1): A

+    MultipleErrors.bpl(14,1): C

+

+Boogie program verifier finished with 0 verified, 3 errors

diff --git a/Test/test7/UnreachableBlocks.bpl b/Test/test7/UnreachableBlocks.bpl
new file mode 100644
index 00000000..6ed287a3
--- /dev/null
+++ b/Test/test7/UnreachableBlocks.bpl
@@ -0,0 +1,40 @@
+// 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

+procedure P()

+{

+entry:

+  goto A;

+A:

+  return;

+B:

+  goto A;

+}

+

+procedure Q()

+{

+entry:

+  goto entry, A;

+A:

+  return;

+}

+

+procedure R()

+{

+entry:

+  return;

+A:

+  goto A;

+}

+

+procedure S()

+{

+entry:

+  return;

+A:

+  goto C;

+B:

+  goto C;

+C:  // C has no dominator

+  return;

+}

diff --git a/Test/test7/runtest.bat b/Test/test7/runtest.bat
new file mode 100644
index 00000000..8da87233
--- /dev/null
+++ b/Test/test7/runtest.bat
@@ -0,0 +1,34 @@
+@echo off

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set BGEXE=%BOOGIEDIR%\Boogie.exe

+

+echo ------------------------------ NestedVC.bpl ---------------------

+%BGEXE% %* /vc:nested NestedVC.bpl

+

+echo ------------------------------ UnreachableBlocks.bpl ---------------------

+%BGEXE% %* /vc:nested UnreachableBlocks.bpl

+

+echo ------------------------------ MultipleErrors.bpl ---------------------

+rem The following tests are rather fickle at the moment--different errors

+rem may be reported during different runs.  Moreover, it is conceivable that

+rem the error trace would be reported in different orders, since we do not

+rem attempt to sort the trace labels at this time.

+rem An interesting thing is that /vc:local can with Simplify report more than one

+rem error for this file, even with /errorLimit:1.  Other than that, only

+rem local and dag produce VCs to which Simplify actually produces different

+rem counterexamples.

+

+setlocal

+for %%f in (block local dag) do (

+  echo.

+  echo ----- /vc:%%f

+  %BGEXE% %* /errorLimit:1 /errorTrace:1 /vc:%%f /logPrefix:-1%%f MultipleErrors.bpl

+)

+for %%f in (local dag) do (

+  echo.

+  echo ----- /errorLimit:10 /vc:%%f

+  %BGEXE% %* /errorLimit:10 /errorTrace:1 /vc:%%f /logPrefix:-10%%f MultipleErrors.bpl

+)

+endlocal