blob: c90930d5820c1691dee67a2e365bb04a38ae8143 (
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
35
36
37
38
39
40
41
42
43
44
|
@echo off
setlocal
set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set BPLEXE=%BOOGIEDIR%\Boogie.exe
REM bugs:
REM Modules1
REM Termination
REM Datatypes
REM NoTypeArgs
REM ReturnTests
REM Predicates
for %%f in (Simple TypeTests NatTypes SmallTests Definedness
FunctionSpecifications ResolutionErrors ParseErrors
Array MultiDimArray NonGhostQuantifiers AdvancedLHS
ModulesCycle Modules0 BadFunction Comprehensions
Basics ControlStructures DTypes ParallelResolveErrors
Parallel TypeParameters Coinductive Corecursion
TypeAntecedents SplitExpr LoopModifies Refinement
RefinementErrors ReturnErrors ChainingDisjointTests
CallStmtTests MultiSets PredExpr LetExpr Skeletons
Maps Compilation) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
if exist %%f.cs. (
del %%f.cs
)
if exist %%f.exe. (
del %%f.exe
)
if exist %%f.dll. (
del %%f.dll
)
if exist %%f.pdb. (
del %%f.pdb
)
if exist %%f.pdb.original. (
del %%f.pdb.original
)
)
|
