diff options
| -rwxr-xr-x | Test/houdini/runtest.py | 72 | ||||
| -rwxr-xr-x | Test/test0/runtest.py | 99 | ||||
| -rwxr-xr-x | Test/test1/runtest.py | 74 | ||||
| -rwxr-xr-x | Test/test13/runtest.py | 62 | ||||
| -rwxr-xr-x | Test/test15/runtest.py | 73 | ||||
| -rwxr-xr-x | Test/test16/runtest.py | 67 | ||||
| -rwxr-xr-x | Test/test17/runtest.py | 65 | ||||
| -rwxr-xr-x | Test/test2/runtest.py | 92 | ||||
| -rwxr-xr-x | Test/test20/runtest.py | 79 | ||||
| -rwxr-xr-x | Test/test21/runtest.py | 90 | ||||
| -rwxr-xr-x | Test/test7/runtest.py | 89 |
11 files changed, 0 insertions, 862 deletions
diff --git a/Test/houdini/runtest.py b/Test/houdini/runtest.py deleted file mode 100755 index 89b38404..00000000 --- a/Test/houdini/runtest.py +++ /dev/null @@ -1,72 +0,0 @@ -#!/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 = ["houd1.bpl", "houd2.bpl", "houd3.bpl", "houd4.bpl", "houd5.bpl", "houd6.bpl", "houd7.bpl", "houd8.bpl", "houd9.bpl", "houd10.bpl", "houd11.bpl", "houd12.bpl"]
-
-for file in files:
- os.system("echo >> Output")
- os.system("echo -------------------- " + file + " -------------------- >> Output")
- runtest("/noinfer /contractInfer /printAssignment " + file)
-
-files = ["test1.bpl", "test2.bpl", "test7.bpl", "test8.bpl", "test9.bpl", "test10.bpl"]
-
-for file in files:
- os.system("echo . >> Output")
- os.system("echo -------------------- " + file + " -------------------- >> Output")
- runtest("/noinfer /contractInfer /printAssignment /inlineDepth:1 " + file)
-
-# 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"
diff --git a/Test/test0/runtest.py b/Test/test0/runtest.py deleted file mode 100755 index 2b240203..00000000 --- a/Test/test0/runtest.py +++ /dev/null @@ -1,99 +0,0 @@ -#!/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 filename == "SeparateVerification0.bpl":
- os.system("echo ----- SeparateVerification0.bpl >> Output")
- elif filename == "SeparateVerification1.bpl SeparateVerification0.bpl":
- os.system("echo ----- SeparateVerification1.bpl SeparateVerification0.bpl >> Output")
- elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl":
- os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl >> Output")
- elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl":
- os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl >> Output")
-
- if os.path.exists("Output"):
- os.system(command + " >> Output")
- else:
- os.system(command + " > Output")
-
-#runtest("Prog0.bpl")
-#runtest("ModifiedBag.bpl")
-runtest("Triggers0.bpl")
-runtest("Triggers1.bpl")
-runtest("/printInstrumented PrettyPrint.bpl")
-runtest("Arrays0.bpl")
-runtest("Arrays1.bpl")
-runtest("Types0.bpl")
-runtest("Types1.bpl")
-runtest("WhereParsing.bpl")
-runtest("WhereParsing0.bpl")
-runtest("WhereParsing1.bpl")
-runtest("WhereParsing2.bpl")
-runtest("WhereResolution.bpl")
-runtest("BadLabels0.bpl")
-runtest("BadLabels1.bpl")
-runtest("LineParse.bpl")
-runtest("LineResolve.bpl")
-runtest("AttributeParsingErr.bpl")
-#runtest("/print:- /env:0 AttributeParsing.bpl")
-runtest("AttributeResolution.bpl")
-#runtest("/print:- /env:0 Quoting.bpl")
-runtest("LargeLiterals0.bpl")
-runtest("MapsResolutionErrors.bpl")
-runtest("Orderings.bpl")
-runtest("BadQuantifier.bpl")
-#runtest("EmptyCallArgs.bpl")
-runtest("SeparateVerification0.bpl")
-runtest("SeparateVerification1.bpl SeparateVerification0.bpl")
-runtest("SeparateVerification0.bpl SeparateVerification0.bpl")
-#runtest("SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.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"
diff --git a/Test/test1/runtest.py b/Test/test1/runtest.py deleted file mode 100755 index 4ef5dd85..00000000 --- a/Test/test1/runtest.py +++ /dev/null @@ -1,74 +0,0 @@ -#!/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")
-
-runtest("Frame0.bpl")
-runtest("Frame1.bpl")
-runtest("LogicalExprs.bpl")
-runtest("Arrays.bpl")
-runtest("WhereTyping.bpl")
-runtest("Family.bpl")
-runtest("AttributeTyping.bpl")
-runtest("UpdateExprTyping.bpl")
-runtest("MapsTypeErrors.bpl")
-runtest("Orderings.bpl")
-runtest("EmptyCallArgs.bpl")
-runtest("FunBody.bpl")
-runtest("IfThenElse0.bpl")
-runtest("Lambda.bpl")
-runtest("IntReal.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"
diff --git a/Test/test13/runtest.py b/Test/test13/runtest.py deleted file mode 100755 index f91fa9f9..00000000 --- a/Test/test13/runtest.py +++ /dev/null @@ -1,62 +0,0 @@ -#!/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 >> Output")
-os.system("echo -------------------- ErrorTraceTestLoopInvViolationBPL -------------------- >> Output")
-runtest("ErrorTraceTestLoopInvViolationBPL.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"
diff --git a/Test/test15/runtest.py b/Test/test15/runtest.py deleted file mode 100755 index ec2b40ca..00000000 --- a/Test/test15/runtest.py +++ /dev/null @@ -1,73 +0,0 @@ -#!/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 = ["NullInModel", "IntInModel", "ModelTest"]
-
-for file in files:
- os.system("echo >> Output")
- os.system("echo -------------------- " + file + " -------------------- >> Output")
- runtest(file + ".bpl /printModel:2")
-
-os.system("echo >> Output")
-os.system("echo -------------------- InterpretedFunctionTests -------------------- >> Output")
-runtest("InterpretedFunctionTests.bpl")
-
-os.system("echo >> Output")
-os.system("echo -------------------- CaptureState -------------------- >> Output")
-runtest("CaptureState.bpl /mv:-")
-
-# 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"
diff --git a/Test/test16/runtest.py b/Test/test16/runtest.py deleted file mode 100755 index 2106e291..00000000 --- a/Test/test16/runtest.py +++ /dev/null @@ -1,67 +0,0 @@ -#!/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"
diff --git a/Test/test17/runtest.py b/Test/test17/runtest.py deleted file mode 100755 index 86681f2a..00000000 --- a/Test/test17/runtest.py +++ /dev/null @@ -1,65 +0,0 @@ -#!/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 = ["contractinfer", "flpydisk"]
-
-for file in files:
- os.system("echo >> Output")
- os.system("echo -------------------- " + file + " -------------------- >> Output")
- runtest("/errorLimit:1 /contractInfer /z3mam:4 /subsumption:0 " + file + ".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"
diff --git a/Test/test2/runtest.py b/Test/test2/runtest.py deleted file mode 100755 index 978343da..00000000 --- a/Test/test2/runtest.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/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"
diff --git a/Test/test20/runtest.py b/Test/test20/runtest.py deleted file mode 100755 index 8617c858..00000000 --- a/Test/test20/runtest.py +++ /dev/null @@ -1,79 +0,0 @@ -#!/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")
-
-runtest("TypeDecls0.bpl")
-runtest("TypeDecls1.bpl")
-runtest("Prog0.bpl")
-runtest("Prog1.bpl")
-runtest("Prog2.bpl")
-runtest("PolyFuns0.bpl")
-runtest("PolyFuns1.bpl")
-runtest("PolyProcs0.bpl")
-runtest("TypeSynonyms0.bpl")
-runtest("TypeSynonyms1.bpl")
-runtest("TypeSynonyms2.bpl")
-runtest("/print:- /env:0 TypeSynonyms0.bpl")
-runtest("/print:- /env:0 /printDesugared TypeSynonyms2.bpl")
-runtest("PolyPolyPoly.bpl")
-runtest("PolyPolyPoly2.bpl")
-runtest("ProcParamReordering.bpl")
-runtest("ParallelAssignment.bpl")
-runtest("ParallelAssignment2.bpl")
-runtest("Coercions.bpl")
-runtest("EmptySeq.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"
diff --git a/Test/test21/runtest.py b/Test/test21/runtest.py deleted file mode 100755 index f42d7665..00000000 --- a/Test/test21/runtest.py +++ /dev/null @@ -1,90 +0,0 @@ -#!/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")
-
-modes = ["n", "p", "a"]
-
-files = ["DisjointDomains.bpl", "DisjointDomains2.bpl", "FunAxioms.bpl",
- "FunAxioms2.bpl", "PolyList.bpl", "Maps0.bpl", "Maps1.bpl",
- "InterestingExamples0.bpl", "InterestingExamples1.bpl", "InterestingExamples2.bpl",
- "InterestingExamples3.bpl", "InterestingExamples4.bpl", "InterestingExamples5.bpl",
- "Colors.bpl", "HeapAbstraction.bpl", "HeapAxiom.bpl", "Triggers0.bpl", "Triggers1.bpl",
- "Keywords.bpl", "Casts.bpl", "BooleanQuantification.bpl", "EmptyList.bpl", "Boxing.bpl",
- "MapOutputTypeParams.bpl", "ParallelAssignment.bpl", "BooleanQuantification2.bpl",
- "Flattening.bpl", "Orderings.bpl", "Orderings2.bpl", "Orderings3.bpl", "Orderings4.bpl",
- "EmptySetBug.bpl", "Coercions2.bpl", "MapAxiomsConsistency.bpl", "LargeLiterals0.bpl",
- "Real.bpl"]
-
-for mode in modes:
- os.system("echo >> Output")
- os.system("echo --------------------- TypeEncoding " + mode + " z3types ---------------------------- >> Output")
- for file in files:
- os.system("echo --------------------- File " + file + " ---------------------------- >> Output")
- runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " " + file)
-
- os.system("echo --------------------- File NameClash.bpl ---------------------------- >> Output")
- runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " NameClash.bpl")
-
- os.system("echo --------------------- File Keywords.bpl ---------------------------- >> Output")
- runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " Keywords.bpl")
-
- os.system("echo --------------------- File LargeLiterals0.bpl ---------------------------- >> Output")
- runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " LargeLiterals0.bpl")
-
- os.system("echo --------------------- File LetSorting.bpl ---------------------------- >> Output")
- runtest("/typeEncoding:" + mode + " /logPrefix:0" + mode + " LetSorting.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"
diff --git a/Test/test7/runtest.py b/Test/test7/runtest.py deleted file mode 100755 index 9b0e557f..00000000 --- a/Test/test7/runtest.py +++ /dev/null @@ -1,89 +0,0 @@ -#!/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 filename == "SeparateVerification0.bpl":
- os.system("echo ----- SeparateVerification0.bpl >> Output")
- elif filename == "SeparateVerification1.bpl SeparateVerification0.bpl":
- os.system("echo ----- SeparateVerification1.bpl SeparateVerification0.bpl >> Output")
- elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl":
- os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl >> Output")
- elif filename == "SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl":
- os.system("echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl >> Output")
-
- if os.path.exists("Output"):
- os.system(command + " >> Output")
- else:
- os.system(command + " > Output")
-
-os.system("echo ------------------------------ NestedVC.bpl --------------------- >> Output")
-runtest("/vc:nested NestedVC.bpl")
-
-os.system("echo ------------------------------ UnreachableBlocks.bpl --------------------- >> Output")
-runtest("/vc:nested UnreachableBlocks.bpl")
-
-os.system("echo ------------------------------ MultipleErrors.bpl --------------------- >> Output")
-
-modes = ["block", "local", "dag"]
-
-for mode in modes:
- os.system("echo >> Output")
- os.system("echo ----- /vc:" + mode + " >> Output")
- runtest("/errorLimit:1 /errorTrace:1 /vc:" + mode + " /logPrefix:-1" + mode + " MultipleErrors.bpl")
-
-modes = ["local", "dag"]
-
-for mode in modes:
- os.system("echo >> Output")
- os.system("echo ----- /errorLimit:10 /vc:" + mode + " >> Output")
- runtest("/errorLimit:10 /errorTrace:1 /vc:" + mode + " /logPrefix:-10" + mode + " MultipleErrors.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"
|