From ed3bd975394f123f1e721e69c5665c189acc7be8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Tue, 25 Jan 2011 09:58:29 +0000
Subject: [PATCH] Required modifications to testcases for submission

---
 pldi2011-testcases/RedBlackTree.scala | 30 ++++++++++++++++++++-------
 run-evaluation                        | 10 +++++++++
 testcases/ListWithSize.scala          |  4 ++--
 3 files changed, 34 insertions(+), 10 deletions(-)

diff --git a/pldi2011-testcases/RedBlackTree.scala b/pldi2011-testcases/RedBlackTree.scala
index 7153bba2f..87d5788af 100644
--- a/pldi2011-testcases/RedBlackTree.scala
+++ b/pldi2011-testcases/RedBlackTree.scala
@@ -66,14 +66,14 @@ object RedBlackTree {
     makeBlack(ins(x, t))
   } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
-//  def buggyAdd(x: Int, t: Tree): Tree = {
-//    require(redNodesHaveBlackChildren(t))
-//    // makeBlack(ins(x, t))
-//    ins(x, t)
-//  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+  def buggyAdd(x: Int, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t))
+    // makeBlack(ins(x, t))
+    ins(x, t)
+  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
   def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
-    require(
+    /*require(
       Node(c,a,x,b) match {
         case Node(Black(),Node(Red(),Node(Red(),a,_,b),_,c),_,d) =>
           redNodesHaveBlackChildren(a) &&
@@ -97,7 +97,7 @@ object RedBlackTree {
           redNodesHaveBlackChildren(d)
         case t => redDescHaveBlackChildren(t)
       }
-    )
+    )*/
     Node(c,a,x,b) match {
       case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) => 
         Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
@@ -109,5 +109,19 @@ object RedBlackTree {
         Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
       case Node(c,a,xV,b) => Node(c,a,xV,b)
     }
-  } ensuring (res => content(res) == content(Node(c,a,x,b)) && redDescHaveBlackChildren(res))
+  } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+  
+  def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+    Node(c,a,x,b) match {
+      case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+    }
+  } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
 }
diff --git a/run-evaluation b/run-evaluation
index 030e8b431..0100f4cc2 100755
--- a/run-evaluation
+++ b/run-evaluation
@@ -3,12 +3,15 @@
 ts=`date +%F-%R`
 pldi="pldi2011-testcases"
 files=( ${pldi}"/AssociativeList.scala" ${pldi}/"InsertionSort.scala" ${pldi}"/RedBlackTree.scala" ${pldi}"/PropositionalLogic.scala" "testcases/ListWithSize.scala")
+#files=( ${pldi}"/RedBlackTree.scala" )
 if [ "$#" -lt "1" ]
 then
   echo "Please provide an unrolling value"
   exit 1
 fi
 
+rm -rf summary
+
 for f in ${files[@]}
 do
   ./funcheck CAV $f
@@ -16,6 +19,13 @@ done
 
 mv summary summary-CAV-${ts}
 
+for f in ${files[@]}
+do
+  ./funcheck CAV prune $f
+done
+
+mv summary summary-CAV-prune-${ts}
+
 for f in ${files[@]}
 do
   ./funcheck PLDI unrolling=${1} $f
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 33a4f7a32..c74a21761 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -97,12 +97,12 @@ object ListWithSize {
 
     def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
       (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
-    } holds
+    } // holds
 
     @induct
     def reverse0exposed(l1 : List, l2 : List) : Boolean = {
       (reverse0(l1, l2) == append(reverse(l1), l2))
-    } holds
+    } // holds
 
     @induct
     def sizeAppend(l1 : List, l2 : List) : Boolean =
-- 
GitLab