From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Test/test7/Answer                | 64 ++++++++++++++++++++++++++++++++++++++++
 Test/test7/MultipleErrors.bpl    | 17 +++++++++++
 Test/test7/NestedVC.bpl          | 21 +++++++++++++
 Test/test7/Output                | 64 ++++++++++++++++++++++++++++++++++++++++
 Test/test7/UnreachableBlocks.bpl | 40 +++++++++++++++++++++++++
 Test/test7/runtest.bat           | 34 +++++++++++++++++++++
 6 files changed, 240 insertions(+)
 create mode 100644 Test/test7/Answer
 create mode 100644 Test/test7/MultipleErrors.bpl
 create mode 100644 Test/test7/NestedVC.bpl
 create mode 100644 Test/test7/Output
 create mode 100644 Test/test7/UnreachableBlocks.bpl
 create mode 100644 Test/test7/runtest.bat

(limited to 'Test/test7')

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
-- 
cgit v1.2.3