diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 12:21:57 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 12:21:57 +0100 |
| commit | 578382b6bd2ace4926e9ed97cf59ec38c7b07797 (patch) | |
| tree | 5ea634e0c5c2881f674c38c5d3b1307c83db8916 /Test/test16/runtest.py | |
| parent | ad34aee0bb9e9090418fd1cb2e2fced7ddb625d8 (diff) | |
| parent | ee4be4f6280d39c31d95e50ac3ac039c6d2ba5f5 (diff) | |
Merge
Diffstat (limited to 'Test/test16/runtest.py')
| -rwxr-xr-x | Test/test16/runtest.py | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/Test/test16/runtest.py b/Test/test16/runtest.py new file mode 100755 index 00000000..2106e291 --- /dev/null +++ b/Test/test16/runtest.py @@ -0,0 +1,67 @@ +#!/usr/bin/python
+
+# 2013 Pantazis Deligiannis
+#
+# runs the test cases of this directory
+
+import sys;
+import os;
+import getopt;
+
+MONO = "/usr/bin/mono "
+BOOGIE = "/Users/pantazis/workspace/boogie/Binaries/Boogie.exe "
+
+PROVER_OPTIONS_Z3 = "/nologo "
+PROVER_OPTIONS_CVC4 = "/proverOpt:SOLVER=cvc4 /nologo "
+
+# choose a parser
+opts, args = getopt.getopt(sys.argv[1:], "s:", ["solver="])
+solver = "Z3"
+for o, a in opts:
+ if o in ("-s", "--solver"):
+ if a == "cvc4":
+ solver = a
+
+# if the Output file exists remove it
+if os.path.exists("Output"):
+ os.remove("Output")
+
+# runs the given test
+def runtest(filename):
+ if solver == "cvc4":
+ if os.name == "nt":
+ command = BOOGIE + PROVER_OPTIONS_CVC4 + filename
+ else:
+ command = MONO + BOOGIE + PROVER_OPTIONS_CVC4 + filename
+ else:
+ if os.name == "nt":
+ command = BOOGIE + PROVER_OPTIONS_Z3 + filename
+ else:
+ command = MONO + BOOGIE + PROVER_OPTIONS_Z3 + filename
+
+ print "===== Testing: " + filename
+
+ if os.path.exists("Output"):
+ os.system(command + " >> Output")
+ else:
+ os.system(command + " > Output")
+
+os.system("echo -------------------- LoopUnroll.bpl /loopUnroll:1 -------------------- >> Output")
+runtest("/loopUnroll:1 /logPrefix:-lu1 LoopUnroll.bpl")
+
+os.system("echo -------------------- LoopUnroll.bpl /loopUnroll:2 -------------------- >> Output")
+runtest("LoopUnroll.bpl /logPrefix:-lu2 /proc:ManyIterations /loopUnroll:2")
+
+os.system("echo -------------------- LoopUnroll.bpl /loopUnroll:3 -------------------- >> Output")
+runtest("LoopUnroll.bpl /logPrefix:-lu3 /proc:ManyIterations /loopUnroll:3")
+
+# compare the output with the expected answers
+test_file = open("Output").readlines()
+correct_file = open("Answer").readlines()
+
+for test, correct in zip(test_file, correct_file):
+ if test.strip(' \t\n\r') != correct.strip(' \t\n\r'):
+ print "\n===== " + os.getcwd().split(os.sep)[-1] + ": FAILED"
+ break
+else:
+ print "\n===== " + os.getcwd().split(os.sep)[-1] + ": PASSED"
|