Dafny: Added tests.

4 files changed, 2 insertions, 28 deletions

diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
index debe2cd3..81ac67ef 100644
--- a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
+++ b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
@@ -1,48 +1,31 @@
 

 -------------------- b1 --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

 Compiled assembly into b1.exe

 

 -------------------- b2 --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

 Compiled assembly into b2.exe

 

 -------------------- b3 --------------------

-b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.

-

-Dafny program verifier finished with 9 verified, 1 error

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

-

-Dafny program verifier finished with 11 verified, 0 errors

 Compiled assembly into b4.dll

 

 -------------------- b5 --------------------

-

-Dafny program verifier finished with 22 verified, 0 errors

 Compiled assembly into b5.dll

 

 -------------------- b6 --------------------

-

-Dafny program verifier finished with 21 verified, 0 errors

 Compiled assembly into b6.exe

 

 -------------------- b7 --------------------

-

-Dafny program verifier finished with 23 verified, 0 errors

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

-

-Dafny program verifier finished with 42 verified, 0 errors

 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

diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking
index 841a04cf..49a440db 100644
--- a/Test/VSI-Benchmarks/AnswerRuntimeChecking
+++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking
@@ -1,29 +1,20 @@
 

 -------------------- b1 --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

 Compiled assembly into b1.exe

 Rewrote assembly into b1.exe

 

 -------------------- b3 --------------------

-b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.

-

-Dafny program verifier finished with 9 verified, 1 error

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

-

-Dafny program verifier finished with 23 verified, 0 errors

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

-

-Dafny program verifier finished with 42 verified, 0 errors

 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

diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
index ccf1ffa8..c85b7606 100644
--- a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
+++ b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
@@ -8,7 +8,7 @@ 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 /runtimeChecking:0 /compile:2 %* %%f.dfy

+  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

   if exist %%f.cs. (

     del %%f.cs

   )

diff --git a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
index 8ac0f707..27df70a3 100644
--- a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
+++ b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
@@ -14,7 +14,7 @@ REM b6: functions
 for %%f in (b1 b3 b7 b8) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

+  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

   if exist %%f.cs. (

     del %%f.cs

   )