diff options
| author |  wuestholz <unknown> | 2013-12-18 11:14:19 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-12-18 11:14:19 +0100 |
| commit | 42d8a89ea406dc001dfd83af2e2d66f5ed813cc7 (patch) | |
| tree | 8f070f6c83aaac5c52016756de016f83a98d2772 /Test/dafny1 | |
| parent | 7a4728f23ce2101c1cfb7668c350f5c9c8953f5c (diff) | |
Add support for the /verifySeparately flag in Boogie and change most tests to use it.
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/runtest.bat | 38 |
1 files changed, 20 insertions, 18 deletions
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 5a43205f..f02a7965 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -4,21 +4,23 @@ setlocal set BINARIES=..\..\Binaries
set DAFNY_EXE=%BINARIES%\Dafny.exe
-for %%f in (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
- ) do (
- echo.
- echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-)
+%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 )
|