From 25c81e8393f0f9d643c223cd3e7f6a734ec65ff5 Mon Sep 17 00:00:00 2001 From: afd Date: Wed, 27 Jun 2012 14:49:15 +0100 Subject: Undo bad merge. --- Test/dafny1/AnswerNoRuntimeChecking | 76 -------------------------------- Test/dafny1/AnswerRuntimeChecking | 27 ------------ Test/dafny1/runtestNoRuntimeChecking.bat | 36 --------------- Test/dafny1/runtestRuntimeChecking.bat | 51 --------------------- 4 files changed, 190 deletions(-) delete mode 100644 Test/dafny1/AnswerNoRuntimeChecking delete mode 100644 Test/dafny1/AnswerRuntimeChecking delete mode 100644 Test/dafny1/runtestNoRuntimeChecking.bat delete mode 100644 Test/dafny1/runtestRuntimeChecking.bat (limited to 'Test/dafny1') 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 - ) -) -- cgit v1.2.3