Merge

2 files changed, 0 insertions, 150 deletions

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
deleted file mode 100644
index e60451c2..00000000
--- a/Test/dafny1/Answer
+++ /dev/null
@@ -1,124 +0,0 @@
-

--------------------- Queue.dfy --------------------

-

-Dafny program verifier finished with 22 verified, 0 errors

-

--------------------- PriorityQueue.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- ExtensibleArray.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

-

--------------------- ExtensibleArrayAuto.dfy --------------------

-

-Dafny program verifier finished with 11 verified, 0 errors

-

--------------------- BinaryTree.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- UnboundedStack.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- SeparationLogicList.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- ListCopy.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-

--------------------- ListReverse.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- ListContents.dfy --------------------

-

-Dafny program verifier finished with 9 verified, 0 errors

-

--------------------- MatrixFun.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- pow2.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- SchorrWaite.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- SchorrWaite-stages.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- Cubes.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- SumOfCubes.dfy --------------------

-

-Dafny program verifier finished with 17 verified, 0 errors

-

--------------------- FindZero.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

-

--------------------- TerminationDemos.dfy --------------------

-

-Dafny program verifier finished with 14 verified, 0 errors

-

--------------------- Substitution.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- TreeDatatype.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- KatzManna.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- Induction.dfy --------------------

-

-Dafny program verifier finished with 33 verified, 0 errors

-

--------------------- Rippling.dfy --------------------

-

-Dafny program verifier finished with 141 verified, 0 errors

-

--------------------- MoreInduction.dfy --------------------

-MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 15 verified, 4 errors

-

--------------------- Celebrity.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

--------------------- BDD.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- UltraFilter.dfy --------------------

-

-Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
deleted file mode 100644
index f02a7965..00000000
--- a/Test/dafny1/runtest.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy

-

-rem for %%f in (Queue.dfy PriorityQueue.dfy

-rem             ExtensibleArray.dfy ExtensibleArrayAuto.dfy

-rem             BinaryTree.dfy

-rem             UnboundedStack.dfy

-rem             SeparationLogicList.dfy

-rem             ListCopy.dfy ListReverse.dfy ListContents.dfy

-rem             MatrixFun.dfy pow2.dfy

-rem             SchorrWaite.dfy SchorrWaite-stages.dfy

-rem             Cubes.dfy SumOfCubes.dfy FindZero.dfy

-rem             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

-rem             Induction.dfy Rippling.dfy MoreInduction.dfy

-rem             Celebrity.dfy BDD.dfy

-rem             UltraFilter.dfy

-rem             ) do (

-rem   echo.

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

-rem   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f

-rem )