From cba3b360f9787ce07c08dc5eda6bb6bec3cddfd1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 28 Sep 2015 14:41:07 +0200
Subject: [PATCH] Add some testcases, focus gitignore

---
 .gitignore                                     | 18 ++++++++++--------
 .../repair/features/focusIfCondition.scala     | 11 +++++++++++
 testcases/repair/features/focusIfElse.scala    | 11 +++++++++++
 testcases/repair/features/focusIfThen.scala    | 11 +++++++++++
 testcases/repair/features/focusLetBody.scala   |  8 ++++++++
 testcases/repair/features/focusMatch.scala     | 16 ++++++++++++++++
 testcases/repair/features/splitIf.scala        | 11 +++++++++++
 testcases/repair/features/splitMatch.scala     | 13 +++++++++++++
 8 files changed, 91 insertions(+), 8 deletions(-)
 create mode 100644 testcases/repair/features/focusIfCondition.scala
 create mode 100644 testcases/repair/features/focusIfElse.scala
 create mode 100644 testcases/repair/features/focusIfThen.scala
 create mode 100644 testcases/repair/features/focusLetBody.scala
 create mode 100644 testcases/repair/features/focusMatch.scala
 create mode 100644 testcases/repair/features/splitIf.scala
 create mode 100644 testcases/repair/features/splitMatch.scala

diff --git a/.gitignore b/.gitignore
index 85f840fd5..f7c7dfdee 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,12 +21,14 @@ target
 derivation*.dot
 
 # leon
-last.log
-*.last
-*.table
-*.log
-smt-sessions/
-leon.out/
+/last.log
+/*.last
+/*.table
+/*.log
+/smt-sessions/
+/leon.out/
+/repairs.dat
+/tmp
 
 #eclipse
 .cache
@@ -41,13 +43,13 @@ Leon.eml
 Leon.iml
 
 #scripts
-out-classes
+/out-classes
 
 #z3
 .z3-trace
 
 #travis
-travis/builds
+/travis/builds
 
 # Isabelle
 contrib
diff --git a/testcases/repair/features/focusIfCondition.scala b/testcases/repair/features/focusIfCondition.scala
new file mode 100644
index 000000000..6209b4036
--- /dev/null
+++ b/testcases/repair/features/focusIfCondition.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a < 0) {
+      -a + 1
+    } else {
+      a
+    }
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusIfElse.scala b/testcases/repair/features/focusIfElse.scala
new file mode 100644
index 000000000..f45927f3d
--- /dev/null
+++ b/testcases/repair/features/focusIfElse.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a > 0) {
+      a
+    } else {
+      BigInt(-1)
+    }
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusIfThen.scala b/testcases/repair/features/focusIfThen.scala
new file mode 100644
index 000000000..211c2b900
--- /dev/null
+++ b/testcases/repair/features/focusIfThen.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a <= 0) {
+      BigInt(-1)
+    } else {
+      a
+    }
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusLetBody.scala b/testcases/repair/features/focusLetBody.scala
new file mode 100644
index 000000000..2a5ed017d
--- /dev/null
+++ b/testcases/repair/features/focusLetBody.scala
@@ -0,0 +1,8 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    val tmp = -a
+    tmp
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusMatch.scala b/testcases/repair/features/focusMatch.scala
new file mode 100644
index 000000000..7795a975e
--- /dev/null
+++ b/testcases/repair/features/focusMatch.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object Test {
+  def focusMatch(a: BigInt, b: BigInt) = {
+    (a, b) match {
+      case (otherA, BigInt(0)) => otherA
+      case _ => a+1
+    }
+  } ensuring {
+    res => if (b == 0) {
+      res == 0
+    } else {
+      res == a+1
+    }
+  }
+}
diff --git a/testcases/repair/features/splitIf.scala b/testcases/repair/features/splitIf.scala
new file mode 100644
index 000000000..18167f777
--- /dev/null
+++ b/testcases/repair/features/splitIf.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a <= 0) {
+      (a, BigInt(0))
+    } else {
+      (a, BigInt(0))
+    }
+  } ensuring {
+    res => res._1 == a && res._2 > 1
+  }
+}
diff --git a/testcases/repair/features/splitMatch.scala b/testcases/repair/features/splitMatch.scala
new file mode 100644
index 000000000..5a6a67758
--- /dev/null
+++ b/testcases/repair/features/splitMatch.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object Test {
+  def focusCond(a: BigInt) = {
+    a match {
+      case BigInt(1) => (BigInt(2), BigInt(0))
+      case BigInt(2) => (BigInt(2), BigInt(0))
+      case _ => (BigInt(0), BigInt(0))
+    }
+  } ensuring {
+    res => res._1 == a && res._2 > 1
+  }
+}
-- 
GitLab