summaryrefslogtreecommitdiff
path: root/Test/dafny0/runtest.bat
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/runtest.bat')
-rw-r--r--Test/dafny0/runtest.bat46
1 files changed, 0 insertions, 46 deletions
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
deleted file mode 100644
index 9118e388..00000000
--- a/Test/dafny0/runtest.bat
+++ /dev/null
@@ -1,46 +0,0 @@
-@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-
-for %%f in (Simple.dfy) do (
- echo.
- echo -------------------- %%f --------------------
- %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f
-)
-
-for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
- FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy
- Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
- ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy
- Comprehensions.dfy Basics.dfy ControlStructures.dfy
- Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
- TypeParameters.dfy Datatypes.dfy
- Coinductive.dfy Corecursion.dfy CoPredicates.dfy
- TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
- LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
- ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
- CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
- Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
- RefinementModificationChecking.dfy TailCalls.dfy
- Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (
- echo.
- echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
-)
-
-for %%f in (Superposition.dfy) do (
- echo.
- echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f
-)
-
-for %%f in (SmallTests.dfy LetExpr.dfy) do (
- echo.
- echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
- %DAFNY_EXE% /compile:0 %* out.tmp.dfy
-)
-
-%DAFNY_EXE% %* Compilation.dfy