4 files changed, 190 insertions, 0 deletions
diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking
new file mode 100644
index 00000000..5472ec14
--- /dev/null
+++ b/Test/dafny1/AnswerNoRuntimeChecking
@@ -0,0 +1,76 @@
+
+-------------------- Queue --------------------
+Compiled assembly into Queue.dll
+
+-------------------- PriorityQueue --------------------
+Compiled assembly into PriorityQueue.dll
+
+-------------------- ExtensibleArray --------------------
+Compiled assembly into ExtensibleArray.exe
+
+-------------------- ExtensibleArrayAuto --------------------
+Compiled assembly into ExtensibleArrayAuto.exe
+
+-------------------- BinaryTree --------------------
+Compiled assembly into BinaryTree.dll
+
+-------------------- UnboundedStack --------------------
+Compiled assembly into UnboundedStack.dll
+
+-------------------- ListCopy --------------------
+Compilation error: an assume statement cannot be compiled (line 14)
+Compilation error: an assume statement cannot be compiled (line 15)
+
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+
+-------------------- ListContents --------------------
+Compiled assembly into ListContents.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+
+-------------------- SchorrWaite --------------------
+Compiled assembly into SchorrWaite.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+
+-------------------- SumOfCubes --------------------
+Compiled assembly into SumOfCubes.dll
+
+-------------------- FindZero --------------------
+Compiled assembly into FindZero.dll
+
+-------------------- TerminationDemos --------------------
+Compiled assembly into TerminationDemos.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compilation error: an assume statement cannot be compiled (line 66)
+
+-------------------- Induction --------------------
+Compiled assembly into Induction.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
+
+-------------------- Celebrity --------------------
+Compilation error: Function _default._default.Knows has no body
+Compilation error: an assume statement cannot be compiled (line 16)
+
+-------------------- BDD --------------------
+Compiled assembly into BDD.dll
+
+-------------------- UltraFilter --------------------
+Compilation error: Method _default.UltraFilter.H has no body
+Compilation error: an assume statement cannot be compiled (line 42)
+Compilation error: an assume statement cannot be compiled (line 45)
+Compilation error: an assume statement cannot be compiled (line 76)
+Compilation error: an assume statement cannot be compiled (line 97)
+Compilation error: an assume statement cannot be compiled (line 98)
diff --git a/Test/dafny1/AnswerRuntimeChecking b/Test/dafny1/AnswerRuntimeChecking
new file mode 100644
index 00000000..1ade5aeb
--- /dev/null
+++ b/Test/dafny1/AnswerRuntimeChecking
@@ -0,0 +1,27 @@
+
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+Rewrote assembly into ListReverse.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+Rewrote assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+Rewrote assembly into pow2.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+Rewrote assembly into Cubes.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+Rewrote assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compiled assembly into KatzManna.dll
+Rewrote assembly into KatzManna.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
diff --git a/Test/dafny1/runtestNoRuntimeChecking.bat b/Test/dafny1/runtestNoRuntimeChecking.bat
new file mode 100644
index 00000000..a4989fa1
--- /dev/null
+++ b/Test/dafny1/runtestNoRuntimeChecking.bat
@@ -0,0 +1,36 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM SeparationLogicList
+REM TreeDatatype
+REM MoreInduction
+
+for %%f in (Queue PriorityQueue ExtensibleArray ExtensibleArrayAuto
+            BinaryTree UnboundedStack ListCopy ListReverse ListContents
+            MatrixFun pow2 SchorrWaite Cubes SumOfCubes FindZero
+            TerminationDemos Substitution KatzManna Induction Rippling
+            Celebrity BDD UltraFilter) do (
+  echo.
+  echo -------------------- %%f --------------------
+  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+  if exist %%f.cs. (
+    del %%f.cs
+  )
+  if exist %%f.exe. (
+    del %%f.exe
+  )
+  if exist %%f.dll. (
+    del %%f.dll
+  )
+  if exist %%f.pdb. (
+    del %%f.pdb
+  )
+  if exist %%f.pdb.original. (
+    del %%f.pdb.original
+  )
+)
diff --git a/Test/dafny1/runtestRuntimeChecking.bat b/Test/dafny1/runtestRuntimeChecking.bat
new file mode 100644
index 00000000..fc32fbf4
--- /dev/null
+++ b/Test/dafny1/runtestRuntimeChecking.bat
@@ -0,0 +1,51 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM bugs:
+REM SeparationLogicList
+REM TreeDatatype
+REM MoreInduction
+
+REM to implement:
+REM Queue              : parallel statements
+REM PriorityQueue      : ghost state
+REM ExtensibleArray    : ghost state
+REM ExtensibleArrayAuto: ghost state
+REM BinaryTree         : old expressions
+REM UnboundedStack     : ghost state
+REM ListCopy           : fresh expressions
+REM ListContents       : old expressions
+REM SchorrWaite        : ghost state
+REM SumOfCubes         : ghost state
+REM FindZero           : ghost state
+REM TerminationDemos   : ghost state
+REM Induction          : quantifiers
+REM Celebrity          : quantifiers
+REM BDD                : ghost state
+REM UltraFilter        : quantifiers
+
+for %%f in (ListReverse MatrixFun pow2 Cubes Substitution KatzManna
+            Rippling) do (
+  echo.
+  echo -------------------- %%f --------------------
+  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+  if exist %%f.cs. (
+    del %%f.cs
+  )
+  if exist %%f.exe. (
+    del %%f.exe
+  )
+  if exist %%f.dll. (
+    del %%f.dll
+  )
+  if exist %%f.pdb. (
+    del %%f.pdb
+  )
+  if exist %%f.pdb.original. (
+    del %%f.pdb.original
+  )
+)