From 91233d8ff9fba3ee3a23c9a95fee72b06e590540 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 16 Dec 2015 18:27:54 +0100
Subject: [PATCH] Fix testcases and report results
---
src/main/scala/leon/repair/Repairman.scala | 2 +-
testcases/repair/List/List5.scala | 8 +-
testcases/repair/List/List7.scala | 2 +-
testcases/repair/runTests.sh | 86 +++++++++++-----------
4 files changed, 49 insertions(+), 49 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 75abd981a..374136471 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -147,7 +147,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val fw = new java.io.FileWriter("repair-report.txt", true)
try {
- fw.write(f"$date: $benchName%-50s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%.2f & & ${timeSynth/1000.0}%.2f $proof%7s \\\\\n")
+ fw.write(f"$date: $benchName%-50s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%.2f & & ${timeSynth/1000.0}%.2f & $proof%7s \\\\\n")
} finally {
fw.close
}
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 743cced65..3c109722c 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -97,11 +97,11 @@ sealed abstract class List[T] {
case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
- //if (h == from) { FIXME
- // Cons(to, r)
- //} else {
+ if (h != from) {
+ Cons(to, r)
+ } else {
Cons(h, r)
- //}
+ }
}} ensuring { res =>
(((this.content -- Set(from)) ++ (if (this.content contains from) Set(to) else Set[T]())) == res.content) &&
res.size == this.size
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index 7eef0585e..41972f4ce 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
}
}} ensuring { res =>
if (this.content contains e) {
- res.isDefined && this.size > res.get && this.apply(res.get) == e
+ res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
} else {
res.isEmpty
}
diff --git a/testcases/repair/runTests.sh b/testcases/repair/runTests.sh
index 55ca5cdf9..5ad1c857c 100755
--- a/testcases/repair/runTests.sh
+++ b/testcases/repair/runTests.sh
@@ -15,53 +15,53 @@ echo "################################" >> $summaryLog
echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog
#All benchmarks:
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler7.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap7.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=insert testcases/repair/Heap/Heap8.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=makeN testcases/repair/Heap/Heap9.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap10.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
+#
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap6.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap7.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert testcases/repair/Heap/Heap8.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN testcases/repair/Heap/Heap9.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap10.scala | tee -a $fullLog
+#
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=pad testcases/repair/List/List1.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=++ testcases/repair/List/List2.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=:+ testcases/repair/List/List3.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --functions=drop testcases/repair/List/List4.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --functions=replace testcases/repair/List/List5.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=count testcases/repair/List/List6.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List7.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List8.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --functions=find testcases/repair/List/List9.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=size testcases/repair/List/List10.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=sum testcases/repair/List/List11.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=- testcases/repair/List/List12.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=drop testcases/repair/List/List13.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=pad testcases/repair/List/List1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=++ testcases/repair/List/List2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=:+ testcases/repair/List/List3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=drop testcases/repair/List/List4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=replace testcases/repair/List/List5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=count testcases/repair/List/List6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List7.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List8.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=find testcases/repair/List/List9.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=size testcases/repair/List/List10.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=sum testcases/repair/List/List11.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=- testcases/repair/List/List12.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=drop testcases/repair/List/List13.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=power testcases/repair/Numerical/Numerical1.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=moddiv testcases/repair/Numerical/Numerical3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=power testcases/repair/Numerical/Numerical1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=moddiv testcases/repair/Numerical/Numerical3.scala | tee -a $fullLog
-
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=split testcases/repair/MergeSort/MergeSort1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort5.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=split testcases/repair/MergeSort/MergeSort1.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort2.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort3.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort4.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort5.scala | tee -a $fullLog
# Average results
-cat $log >> $summaryLog
-awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
+#cat $log >> $summaryLog
+#awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
--
GitLab