Undo bad merge.

4 files changed, 0 insertions, 190 deletions

diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking
deleted file mode 100644
index 5472ec14..00000000
--- a/Test/dafny1/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,76 +0,0 @@
-

--------------------- 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
deleted file mode 100644
index 1ade5aeb..00000000
--- a/Test/dafny1/AnswerRuntimeChecking
+++ /dev/null
@@ -1,27 +0,0 @@
-

--------------------- 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
deleted file mode 100644
index a4989fa1..00000000
--- a/Test/dafny1/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,36 +0,0 @@
-@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
deleted file mode 100644
index fc32fbf4..00000000
--- a/Test/dafny1/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,51 +0,0 @@
-@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

-  )

-)