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/vstte2012/AnswerNoRuntimeChecking | 18 ---------------- Test/vstte2012/AnswerRuntimeChecking | 11 ---------- Test/vstte2012/runtestNoRuntimeChecking.bat | 28 ------------------------- Test/vstte2012/runtestRuntimeChecking.bat | 32 ----------------------------- 4 files changed, 89 deletions(-) delete mode 100644 Test/vstte2012/AnswerNoRuntimeChecking delete mode 100644 Test/vstte2012/AnswerRuntimeChecking delete mode 100644 Test/vstte2012/runtestNoRuntimeChecking.bat delete mode 100644 Test/vstte2012/runtestRuntimeChecking.bat (limited to 'Test/vstte2012') diff --git a/Test/vstte2012/AnswerNoRuntimeChecking b/Test/vstte2012/AnswerNoRuntimeChecking deleted file mode 100644 index c5508749..00000000 --- a/Test/vstte2012/AnswerNoRuntimeChecking +++ /dev/null @@ -1,18 +0,0 @@ - --------------------- Two-Way-Sort -------------------- -Compiled assembly into Two-Way-Sort.dll - --------------------- Combinators -------------------- -Compiled assembly into Combinators.dll - --------------------- RingBuffer -------------------- -Compiled assembly into RingBuffer.dll - --------------------- RingBufferAuto -------------------- -Compiled assembly into RingBufferAuto.dll - --------------------- Tree -------------------- -Compiled assembly into Tree.dll - --------------------- BreadthFirstSearch -------------------- -Compilation error: Function _default.BreadthFirstSearch.Succ has no body diff --git a/Test/vstte2012/AnswerRuntimeChecking b/Test/vstte2012/AnswerRuntimeChecking deleted file mode 100644 index 5c703cc7..00000000 --- a/Test/vstte2012/AnswerRuntimeChecking +++ /dev/null @@ -1,11 +0,0 @@ - --------------------- Two-Way-Sort -------------------- -Compiled assembly into Two-Way-Sort.dll -Rewrote assembly into Two-Way-Sort.dll - --------------------- Tree -------------------- -Compiled assembly into Tree.dll -Rewrote assembly into Tree.dll - --------------------- BreadthFirstSearch -------------------- -Compilation error: Function _default.BreadthFirstSearch.Succ has no body diff --git a/Test/vstte2012/runtestNoRuntimeChecking.bat b/Test/vstte2012/runtestNoRuntimeChecking.bat deleted file mode 100644 index e572ed2f..00000000 --- a/Test/vstte2012/runtestNoRuntimeChecking.bat +++ /dev/null @@ -1,28 +0,0 @@ -@echo off -setlocal - -set BOOGIEDIR=..\..\Binaries -set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe - -for %%f in (Two-Way-Sort Combinators RingBuffer RingBufferAuto - Tree BreadthFirstSearch) 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/vstte2012/runtestRuntimeChecking.bat b/Test/vstte2012/runtestRuntimeChecking.bat deleted file mode 100644 index 042efe96..00000000 --- a/Test/vstte2012/runtestRuntimeChecking.bat +++ /dev/null @@ -1,32 +0,0 @@ -@echo off -setlocal - -set BOOGIEDIR=..\..\Binaries -set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe -set BPLEXE=%BOOGIEDIR%\Boogie.exe - -REM to implement: -REM Combinators : ghost state -REM RingBuffer : ghost state -REM RingBufferAuto: ghost state - -for %%f in (Two-Way-Sort Tree BreadthFirstSearch) 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