diff options
| author |  afd <unknown> | 2012-06-27 14:49:15 +0100 |
|---|---|---|
| committer | afd <unknown> | 2012-06-27 14:49:15 +0100 |
| commit | 25c81e8393f0f9d643c223cd3e7f6a734ec65ff5 (patch) | |
| tree | fb816688709524ef44134a9a4397f7abdcd0e267 /Test/vstte2012 | |
| parent | 65d7648ad268f8670246be96c76afdf53ccae871 (diff) | |
Undo bad merge.
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/AnswerNoRuntimeChecking | 18 | ||||
| -rw-r--r-- | Test/vstte2012/AnswerRuntimeChecking | 11 | ||||
| -rw-r--r-- | Test/vstte2012/runtestNoRuntimeChecking.bat | 28 | ||||
| -rw-r--r-- | Test/vstte2012/runtestRuntimeChecking.bat | 32 |
4 files changed, 0 insertions, 89 deletions
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
- )
-)
|