From 39a8abe0d2d6e4bda54fb3a481b049c19fe1dba9 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 1 Jul 2014 17:52:52 +0200 Subject: Removed the old test infrastructure. --- Test/dafny1/Answer | 124 ------------------------------------------------ Test/dafny1/runtest.bat | 26 ---------- 2 files changed, 150 deletions(-) delete mode 100644 Test/dafny1/Answer delete mode 100644 Test/dafny1/runtest.bat (limited to 'Test/dafny1') 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 ) -- cgit v1.2.3