Dafny: Added tests.

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

+  )

+)