summaryrefslogtreecommitdiff
path: root/Test/AbsHoudini/runtest.bat
diff options
context:
space:
mode:
authorGravatar Unknown <akashl@akash-desk.fareast.corp.microsoft.com>2012-11-05 15:52:27 +0530
committerGravatar Unknown <akashl@akash-desk.fareast.corp.microsoft.com>2012-11-05 15:52:27 +0530
commit8cc5d9cc9d455b42fc19881f29da47a08f10d8e1 (patch)
treeea6223c6b4ced1492e832f35d0229e25c86a06ab /Test/AbsHoudini/runtest.bat
parentda91e455665b6874af1af29aed37599247f5ece5 (diff)
Added Abstract Houdini: an implementation of Houdini based on abstract domains.
Currently only predicate-abstraction domain is supported.
Diffstat (limited to 'Test/AbsHoudini/runtest.bat')
-rw-r--r--Test/AbsHoudini/runtest.bat11
1 files changed, 11 insertions, 0 deletions
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
new file mode 100644
index 00000000..34308e4e
--- /dev/null
+++ b/Test/AbsHoudini/runtest.bat
@@ -0,0 +1,11 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (f1.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f
+)
+