summaryrefslogtreecommitdiff
path: root/Test/inline/runtest.bat
diff options
context:
space:
mode:
Diffstat (limited to 'Test/inline/runtest.bat')
-rw-r--r--Test/inline/runtest.bat43
1 files changed, 0 insertions, 43 deletions
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
deleted file mode 100644
index f025de1b..00000000
--- a/Test/inline/runtest.bat
+++ /dev/null
@@ -1,43 +0,0 @@
-@echo off
-setlocal
-
-set BGEXE=..\..\Binaries\Boogie.exe
-
-for %%f in (test0.bpl codeexpr.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 (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
-
-echo -------------------- InliningAndLoops.bpl --------------------
-%BGEXE% %* /loopUnroll:3 /soundLoopUnrolling InliningAndLoops.bpl
-