From 2e803d553c8f579891a97a0c666e8b29044ff9d0 Mon Sep 17 00:00:00 2001
From: chmaria <unknown>
Date: Mon, 11 Jun 2012 08:54:00 +0200
Subject: Dafny: Added compiler tests.

---
 Test/VSI-Benchmarks/AnswerNoRuntimeChecking      | 49 ++++++++++++++++++++++++
 Test/VSI-Benchmarks/AnswerRuntimeChecking        | 30 +++++++++++++++
 Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat | 27 +++++++++++++
 Test/VSI-Benchmarks/runtestRuntimeChecking.bat   | 33 ++++++++++++++++
 4 files changed, 139 insertions(+)
 create mode 100644 Test/VSI-Benchmarks/AnswerNoRuntimeChecking
 create mode 100644 Test/VSI-Benchmarks/AnswerRuntimeChecking
 create mode 100644 Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
 create mode 100644 Test/VSI-Benchmarks/runtestRuntimeChecking.bat

(limited to 'Test/VSI-Benchmarks')

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
+  )
+)
-- 
cgit v1.2.3