From 617a070d0bbfce015033a3b1b7b1cf7aa1b16a86 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 3 Feb 2015 12:13:26 +0100
Subject: [PATCH] Fix runtests/ add List benchmarks
---
runTests.sh | 47 +++++++++++++++++++------------
testcases/repair/List/List4.scala | 6 ++--
testcases/repair/List/List5.scala | 4 ++-
3 files changed, 35 insertions(+), 22 deletions(-)
diff --git a/runTests.sh b/runTests.sh
index 1e71fac49..eaa74b8c0 100755
--- a/runTests.sh
+++ b/runTests.sh
@@ -13,24 +13,35 @@ echo "################################" >> $fullLog
echo "# Category, File, function, S, f.S, Tms, Fms, Rms, verif?" >> $fullLog
#All benchmarks:
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala
-
-./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala
-./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala
-./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort8.scala
-./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort6.scala
-./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort7.scala
-./leon --repair --solvers=fairz3:enum --functions=insert testcases/repair/HeapSort/HeapSort5.scala
-./leon --repair --solvers=fairz3:enum --functions=makeN testcases/repair/HeapSort/HeapSort9.scala
-
-./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala
-./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala
-./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala
-./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala
-./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala
+
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort5.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort6.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort7.scala
+./leon --repair --solvers=fairz3:enum --functions=insert testcases/repair/HeapSort/HeapSort8.scala
+./leon --repair --solvers=fairz3:enum --functions=makeN testcases/repair/HeapSort/HeapSort9.scala
+
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala
+
+./leon --repair --solvers=fairz3:enum --functions=_pad testcases/repair/List/List1.scala
+./leon --repair --solvers=fairz3:enum --functions=_ap testcases/repair/List/List3.scala
+./leon --repair --functions=_drop testcases/repair/List/List4.scala
+./leon --repair --functions=_replace testcases/repair/List/List5.scala
+./leon --repair --solvers=fairz3:enum --functions=_count testcases/repair/List/List6.scala
+./leon --repair --solvers=fairz3:enum --functions=_find testcases/repair/List/List7.scala
+./leon --repair --solvers=fairz3:enum --functions=_find testcases/repair/List/List8.scala
+./leon --repair --functions=_find testcases/repair/List/List9.scala
+./leon --repair --solvers=fairz3:enum --functions=_size testcases/repair/List/List10.scala
+./leon --repair --solvers=fairz3:enum --functions=sum testcases/repair/List/List11.scala
# Average results
cat $log >> $fullLog
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index 210a5544b..6bee40d15 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -82,9 +82,9 @@ sealed abstract class List0[T] {
case (Cons0(h, t), i) =>
t.drop(i-1) //FIXME missing if-split
}} ensuring { res => ((this, i), res) passes {
- case (l@Cons0(_, Nil0()), 42) => l
- case (Cons0(a, t), 0) => t
- case (Cons0(a, Cons0(b, Nil0())), 1) => Cons0(a, Nil0())
+ case (Cons0(_, Nil0()), 42) => Nil0()
+ case (l@Cons0(_, _), 0) => l
+ case (Cons0(a, Cons0(b, Nil0())), 1) => Cons0(b, Nil0())
}}
def slice(from: Int, to: Int): List0[T] = {
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 266f4037f..82e604eaf 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -97,7 +97,9 @@ sealed abstract class List0[T] {
case Cons0(h, t) =>
val r = t.replace(from, to)
Cons0(to, r) // FIXME
- }} ensuring { res => (res.content == this.content -- Set(from) ++ Set(to)) && res.size == this.size
+ }} ensuring { res =>
+ (if(this.contains(from)) res.contains(to) else true) &&
+ !res.contains(from) && res.size == this.size
}
private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
--
GitLab