diff options
| author |  chmaria <unknown> | 2012-06-11 08:54:00 +0200 |
|---|---|---|
| committer | chmaria <unknown> | 2012-06-11 08:54:00 +0200 |
| commit | 2e803d553c8f579891a97a0c666e8b29044ff9d0 (patch) | |
| tree | 632c57fd61f7fb01bf71aa3a39a185300f123aa2 /Test/VSI-Benchmarks | |
| parent | efb3a31b7d5454778b84b3d91fceae5972bffd8d (diff) | |
Dafny: Added compiler tests.
Diffstat (limited to 'Test/VSI-Benchmarks')
| -rw-r--r-- | Test/VSI-Benchmarks/AnswerNoRuntimeChecking | 49 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/AnswerRuntimeChecking | 30 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat | 27 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/runtestRuntimeChecking.bat | 33 |
4 files changed, 139 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking new file mode 100644 index 00000000..debe2cd3 --- /dev/null +++ b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking @@ -0,0 +1,49 @@ +
+-------------------- 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
+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..841a04cf --- /dev/null +++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking @@ -0,0 +1,30 @@ +
+-------------------- 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
+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..ccf1ffa8 --- /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 /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..8ac0f707 --- /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 /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
+ )
+)
|