diff options
Diffstat (limited to 'Test/VSI-Benchmarks')
-rw-r--r-- | Test/VSI-Benchmarks/AnswerNoRuntimeChecking | 32 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/AnswerRuntimeChecking | 21 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat | 27 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/runtestRuntimeChecking.bat | 33 |
4 files changed, 113 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking new file mode 100644 index 00000000..81ac67ef --- /dev/null +++ b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking @@ -0,0 +1,32 @@ +
+-------------------- b1 --------------------
+Compiled assembly into b1.exe
+
+-------------------- b2 --------------------
+Compiled assembly into b2.exe
+
+-------------------- b3 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+
+-------------------- b4 --------------------
+Compiled assembly into b4.dll
+
+-------------------- b5 --------------------
+Compiled assembly into b5.dll
+
+-------------------- b6 --------------------
+Compiled assembly into b6.exe
+
+-------------------- b7 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Client.Sort has no body
+
+-------------------- b8 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking new file mode 100644 index 00000000..49a440db --- /dev/null +++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking @@ -0,0 +1,21 @@ +
+-------------------- b1 --------------------
+Compiled assembly into b1.exe
+Rewrote assembly into b1.exe
+
+-------------------- b3 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+
+-------------------- b7 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Client.Sort has no body
+
+-------------------- b8 --------------------
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat new file mode 100644 index 00000000..c85b7606 --- /dev/null +++ b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat @@ -0,0 +1,27 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (b1 b2 b3 b4 b5 b6 b7 b8) 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/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat new file mode 100644 index 00000000..27df70a3 --- /dev/null +++ b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat @@ -0,0 +1,33 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM b2: quantifiers
+REM b4: old expressions
+REM b5: parallel statements
+REM b6: functions
+
+for %%f in (b1 b3 b7 b8) 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
+ )
+)
|