blob: c4bc5d824f8cd64d72fb62ec0a40abdc840b0202 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
@echo off
setlocal
set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set BPLEXE=%BOOGIEDIR%\Boogie.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
Modules0.dfy Modules1.dfy BadFunction.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
LoopModifies.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
)
for %%f in (SmallTests.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
%DAFNY_EXE% /compile:0 %* out.tmp.dfy
)
|
