Undo bad merge.

4 files changed, 0 insertions, 110 deletions

diff --git a/Test/dafny2/AnswerNoRuntimeChecking b/Test/dafny2/AnswerNoRuntimeChecking
deleted file mode 100644
index f04bb934..00000000
--- a/Test/dafny2/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,30 +0,0 @@
-

--------------------- Classics --------------------

-Compiled assembly into Classics.dll

-

--------------------- TreeBarrier --------------------

-Compilation error: an assume statement cannot be compiled (line 90)

-Compilation error: an assume statement cannot be compiled (line 102)

-Compilation error: an assume statement cannot be compiled (line 128)

-

--------------------- COST-verif-comp-2011-1-MaxArray --------------------

-Compiled assembly into COST-verif-comp-2011-1-MaxArray.dll

-

--------------------- COST-verif-comp-2011-2-MaxTree-class --------------------

-Compiled assembly into COST-verif-comp-2011-2-MaxTree-class.dll

-

--------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------

-Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll

-

--------------------- COST-verif-comp-2011-3-TwoDuplicates --------------------

-Compiled assembly into COST-verif-comp-2011-3-TwoDuplicates.dll

-

--------------------- COST-verif-comp-2011-4-FloydCycleDetect --------------------

-Compiled assembly into COST-verif-comp-2011-4-FloydCycleDetect.dll

-

--------------------- Intervals --------------------

-Compiled assembly into Intervals.dll

-

--------------------- StoreAndRetrieve --------------------

-Compilation error: an assume statement cannot be compiled (line 21)

-Compilation error: Function Library.Function.Apply has no body

diff --git a/Test/dafny2/AnswerRuntimeChecking b/Test/dafny2/AnswerRuntimeChecking
deleted file mode 100644
index 32b61bb1..00000000
--- a/Test/dafny2/AnswerRuntimeChecking
+++ /dev/null
@@ -1,7 +0,0 @@
-

--------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------

-Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll

-Rewrote assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll

-

--------------------- StoreAndRetrieve --------------------

-Compilation error: Function Library.Function.Apply has no body

diff --git a/Test/dafny2/runtestNoRuntimeChecking.bat b/Test/dafny2/runtestNoRuntimeChecking.bat
deleted file mode 100644
index b60fd69c..00000000
--- a/Test/dafny2/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,34 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM soon again: SnapshotableTrees.dfy

-

-for %%f in (Classics TreeBarrier COST-verif-comp-2011-1-MaxArray

-            COST-verif-comp-2011-2-MaxTree-class

-            COST-verif-comp-2011-2-MaxTree-datatype

-            COST-verif-comp-2011-3-TwoDuplicates

-            COST-verif-comp-2011-4-FloydCycleDetect

-            Intervals StoreAndRetrieve) 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/dafny2/runtestRuntimeChecking.bat b/Test/dafny2/runtestRuntimeChecking.bat
deleted file mode 100644
index 4ba447a7..00000000
--- a/Test/dafny2/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,39 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM soon again: SnapshotableTrees.dfy

-

-REM to implement:

-REM Classics                               : ghost state

-REM TreeBarrier                            : ghost state

-REM COST-verif-comp-2011-1-MaxArray        : ghost state

-REM COST-verif-comp-2011-2-MaxTree-class   : ghost state

-REM COST-verif-comp-2011-3-TwoDuplicates   : quantifiers

-REM COST-verif-comp-2011-4-FloydCycleDetect: quantifiers

-REM Intervals                              : ghost state

-

-for %%f in (COST-verif-comp-2011-2-MaxTree-datatype

-            StoreAndRetrieve) 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

-  )

-)