From a6ad13aab30cd2bdd9576c74bf58e7e2b9b855d5 Mon Sep 17 00:00:00 2001
From: Pantazis Deligiannis <pdeligia@me.com>
Date: Sun, 7 Jul 2013 03:18:00 +0100
Subject: added python scripts (work in unix and windows) for testing Z3 and
 CVC4 to many of the test suite dirs

---
 Test/test2/runtest.py | 92 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100755 Test/test2/runtest.py

(limited to 'Test/test2')

diff --git a/Test/test2/runtest.py b/Test/test2/runtest.py
new file mode 100755
index 00000000..978343da
--- /dev/null
+++ b/Test/test2/runtest.py
@@ -0,0 +1,92 @@
+#!/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")
+
+files = ["FormulaTerm.bpl", "FormulaTerm2.bpl", "Passification.bpl", "B.bpl",
+  "Ensures.bpl", "Old.bpl", "OldIllegal.bpl", "Arrays.bpl", "Axioms.bpl",
+  "Quantifiers.bpl", "Call.bpl", "AssumeEnsures.bpl",
+  "CutBackEdge.bpl", "False.bpl", "LoopInvAssume.bpl",
+  "strings-no-where.bpl", "strings-where.bpl",
+  "Structured.bpl", "Where.bpl", "UpdateExpr.bpl",
+  "NeverPattern.bpl", "NullaryMaps.bpl", "Implies.bpl",
+  "IfThenElse1.bpl", "Lambda.bpl", "LambdaPoly.bpl", "LambdaOldExpressions.bpl",
+  "SelectiveChecking.bpl", "FreeCall.bpl"]
+
+for file in files:
+  os.system("echo >> Output")
+  os.system("echo -------------------- " + file + " -------------------- >> Output")
+  runtest("/noinfer " + file)
+  
+files = ["Arrays.bpl", "Lambda.bpl", "TypeEncodingM.bpl"]
+
+for file in files:
+  os.system("echo >> Output")
+  os.system("echo -------------------- " + file + " /typeEncoding:m -------------------- >> Output")
+  runtest("/noinfer /typeEncoding:m " + file)
+  
+os.system("echo >> Output")
+os.system("echo -------------------- sk_hack.bpl -------------------- >> Output")
+runtest("/noinfer sk_hack.bpl")
+
+os.system("echo >> Output")
+os.system("echo -------------------- ContractEvaluationOrder.bpl -------------------- >> Output")
+runtest("ContractEvaluationOrder.bpl")
+
+os.system("echo >> Output")
+os.system("echo -------------------- Timeouts0.bpl -------------------- >> Output")
+runtest("/timeLimit:4 Timeouts0.bpl")
+
+# 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"
-- 
cgit v1.2.3