blob: 3a8b0a9d857ae6001239c51e290f3d48f94b144d (
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 BGEXE=..\..\Binaries\Boogie.exe
for %%f in (test0.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f
)
for %%f in (test7.bpl test8.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* /inline:spec /inlineDepth:1 /print:- /env:0 /printInlined /noinfer %%f
)
for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
REM Peephole optimizations are so good that Elevator seems worthwhile
REM to include twice among these inline tests
for %%f in (Elevator.bpl) do (
echo -------------------- %%f with empty blocks --------------------
%BGEXE% /removeEmptyBlocks:0 %* %%f
)
echo -------------------- expansion2.bpl --------------------
%BGEXE% %* /proverLog:expansion2.sx expansion2.bpl
%SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx
%SystemRoot%\system32\find.exe /C "xxf1" expansion2.sx
echo -------------------- fundef.bpl --------------------
%BGEXE% %* /print:- /env:0 fundef.bpl
%BGEXE% %* fundef2.bpl
echo -------------------- polyInline.bpl --------------------
%BGEXE% %* /typeEncoding:predicates /logPrefix:p polyInline.bpl
%BGEXE% %* /typeEncoding:arguments /logPrefix:a polyInline.bpl
|
