From 2b186ade649770402c4dd6ab72bc8455e5b24f45 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 5 Mar 2012 18:04:27 +0100
Subject: [PATCH] Scala 2.9.1-1 and refactored testcases
---
build.sbt | 4 ++--
testcases/AddressBook.scala | 4 ++--
testcases/ConnectedTest.scala | 4 ++--
testcases/Expr2Comp.scala | 6 +++---
testcases/ExprComp.scala | 4 ++--
testcases/InsertionSort.scala | 2 +-
testcases/IntOperations.scala | 2 +-
testcases/ListWithSize.scala | 4 ++--
testcases/MutuallyRecursive.scala | 4 ++--
testcases/Naturals.scala | 4 ++--
testcases/README | 2 +-
testcases/Test.scala | 4 ++--
testcases/TwoSizeFunctions.scala | 4 ++--
testcases/UseContradictoryLemma.scala | 4 ++--
testcases/VerySimple.scala | 4 ++--
testcases/Viktor.scala | 2 +-
testcases/pldi2011-testcases/AssociativeList.scala | 4 ++--
testcases/pldi2011-testcases/ForElimination.scala | 4 ++--
testcases/pldi2011-testcases/InsertionSort.scala | 4 ++--
testcases/pldi2011-testcases/LambdaEval.scala | 4 ++--
testcases/pldi2011-testcases/PropositionalLogic.scala | 4 ++--
testcases/pldi2011-testcases/QuickSort.scala | 4 ++--
testcases/pldi2011-testcases/RedBlackTree.scala | 4 ++--
testcases/pldi2011-testcases/RedBlackTreeDeletion.scala | 2 +-
testcases/pldi2011-testcases/SemanticsPreservation.scala | 4 ++--
testcases/pldi2011-testcases/TreeMap.scala | 2 +-
testcases/sas2011-testcases/AmortizedQueue.scala | 4 ++--
testcases/sas2011-testcases/AssociativeList.scala | 4 ++--
testcases/sas2011-testcases/InsertionSort.scala | 4 ++--
testcases/sas2011-testcases/PropositionalLogic.scala | 4 ++--
testcases/sas2011-testcases/RedBlackTree.scala | 4 ++--
testcases/sas2011-testcases/SearchLinkedList.scala | 4 ++--
testcases/sas2011-testcases/SumAndMax.scala | 4 ++--
testcases/vmcai2011-testcases/JustFormulas.scala | 2 +-
testcases/vmcai2011-testcases/SanityChecks.scala | 2 +-
testcases/vstte10competition/AmortizedQueue.scala | 4 ++--
testcases/vstte10competition/Injection.scala | 4 ++--
testcases/vstte10competition/SearchLinkedList.scala | 4 ++--
testcases/vstte10competition/SumAndMax.scala | 4 ++--
39 files changed, 71 insertions(+), 71 deletions(-)
diff --git a/build.sbt b/build.sbt
index 908d231bc..9c65cad86 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,13 +4,13 @@ version := "2.0"
organization := "ch.epfl.lara"
-scalaVersion := "2.9.0-1"
+scalaVersion := "2.9.1-1"
scalacOptions += "-deprecation"
scalacOptions += "-unchecked"
-libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.0-1"
+libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.1-1"
unmanagedBase <<= baseDirectory { base => base / "unmanaged" }
diff --git a/testcases/AddressBook.scala b/testcases/AddressBook.scala
index 9e5144ceb..aaad0040a 100644
--- a/testcases/AddressBook.scala
+++ b/testcases/AddressBook.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
// Ongoing work: take Chapter 2 of Daniel Jackson's book,
// adapt the addressbook example from there.
diff --git a/testcases/ConnectedTest.scala b/testcases/ConnectedTest.scala
index a50e3cd24..001259852 100644
--- a/testcases/ConnectedTest.scala
+++ b/testcases/ConnectedTest.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object VerySimple {
sealed abstract class L0
diff --git a/testcases/Expr2Comp.scala b/testcases/Expr2Comp.scala
index b5aa14adc..eca1fe6f5 100644
--- a/testcases/Expr2Comp.scala
+++ b/testcases/Expr2Comp.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object ExprComp {
// Lists
@@ -111,7 +111,7 @@ object ExprComp {
def main(args : Array[String]) = {
val e1 = Binary(Constant(100), Times(), Binary(Constant(3), Plus(), Constant(5)))
- // thanks to funcheck:
+ // thanks to Leon:
val e = Binary(Binary(Binary(Binary(Constant(75), Plus(), Constant(69)), Times(), Binary(Constant(73), Plus(), Constant(71))), Times(), Binary(Binary(Constant(70), Plus(), Constant(77)), Times(), Binary(Constant(68), Plus(), Constant(66)))), Plus(), Binary(Constant(1), Plus(), Binary(Constant(0), Times(), Binary(Constant(65), Plus(), Constant(72)))))
val acc = EProgram()
val vs = Cons(42,Nil())
diff --git a/testcases/ExprComp.scala b/testcases/ExprComp.scala
index fb36237dc..116f0099b 100644
--- a/testcases/ExprComp.scala
+++ b/testcases/ExprComp.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object ExprComp {
diff --git a/testcases/InsertionSort.scala b/testcases/InsertionSort.scala
index 0db222160..6b162246f 100644
--- a/testcases/InsertionSort.scala
+++ b/testcases/InsertionSort.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
+import leon.Utils._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/IntOperations.scala b/testcases/IntOperations.scala
index 98a757434..98c9f9e5f 100644
--- a/testcases/IntOperations.scala
+++ b/testcases/IntOperations.scala
@@ -9,7 +9,7 @@ object IntOperations {
// The body of the following function is not in PureScala
// It will still get extracted, with "unknown body".
- // To disable the warnings, run with -P:funcheck:tolerant
+ // To disable the warnings, run with -P:leon:tolerant
// (if it has a postcondition, you'll still get warnings
// about the impossibility of verifying them)
def factorial(v: Int) : Int = {
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index c74a21761..868cb4556 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object ListWithSize {
sealed abstract class List
diff --git a/testcases/MutuallyRecursive.scala b/testcases/MutuallyRecursive.scala
index 374b571c7..bd5a6bfe4 100644
--- a/testcases/MutuallyRecursive.scala
+++ b/testcases/MutuallyRecursive.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object MutuallyRecursive {
def f(n : Int) : Int = {
diff --git a/testcases/Naturals.scala b/testcases/Naturals.scala
index 8f9ea8315..9b621b0a0 100644
--- a/testcases/Naturals.scala
+++ b/testcases/Naturals.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object Naturals {
sealed abstract class Nat
diff --git a/testcases/README b/testcases/README
index 020435430..896a958ee 100644
--- a/testcases/README
+++ b/testcases/README
@@ -1,2 +1,2 @@
-Anything that's in this directory needs to be parsable by FunCheck, otherwise
+Anything that's in this directory needs to be parsable by Leon, otherwise
it will make me angry.
diff --git a/testcases/Test.scala b/testcases/Test.scala
index 798ee0037..79f143b34 100644
--- a/testcases/Test.scala
+++ b/testcases/Test.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object Test {
sealed abstract class List
diff --git a/testcases/TwoSizeFunctions.scala b/testcases/TwoSizeFunctions.scala
index 1e9990741..e88239783 100644
--- a/testcases/TwoSizeFunctions.scala
+++ b/testcases/TwoSizeFunctions.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object TwoSizeFunctions {
sealed abstract class List
diff --git a/testcases/UseContradictoryLemma.scala b/testcases/UseContradictoryLemma.scala
index f25cec124..5ab165bfc 100644
--- a/testcases/UseContradictoryLemma.scala
+++ b/testcases/UseContradictoryLemma.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object UseContradictoryLemma {
diff --git a/testcases/VerySimple.scala b/testcases/VerySimple.scala
index b2f5977eb..d89391d42 100644
--- a/testcases/VerySimple.scala
+++ b/testcases/VerySimple.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object VerySimple {
sealed abstract class List
diff --git a/testcases/Viktor.scala b/testcases/Viktor.scala
index 009953cd8..3d86ee0ff 100644
--- a/testcases/Viktor.scala
+++ b/testcases/Viktor.scala
@@ -1,4 +1,4 @@
-import funcheck.Utils._
+import leon.Utils._
object Viktor {
def transitive(x: Boolean, y: Boolean, z: Boolean) : Boolean = {
diff --git a/testcases/pldi2011-testcases/AssociativeList.scala b/testcases/pldi2011-testcases/AssociativeList.scala
index ed18a6bba..6b9319afd 100644
--- a/testcases/pldi2011-testcases/AssociativeList.scala
+++ b/testcases/pldi2011-testcases/AssociativeList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AssociativeList {
sealed abstract class KeyValuePairAbs
diff --git a/testcases/pldi2011-testcases/ForElimination.scala b/testcases/pldi2011-testcases/ForElimination.scala
index df39b2bc4..ed8e6b877 100644
--- a/testcases/pldi2011-testcases/ForElimination.scala
+++ b/testcases/pldi2011-testcases/ForElimination.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object ForElimination {
diff --git a/testcases/pldi2011-testcases/InsertionSort.scala b/testcases/pldi2011-testcases/InsertionSort.scala
index 7d5e0eb62..a1215b025 100644
--- a/testcases/pldi2011-testcases/InsertionSort.scala
+++ b/testcases/pldi2011-testcases/InsertionSort.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/pldi2011-testcases/LambdaEval.scala b/testcases/pldi2011-testcases/LambdaEval.scala
index 889847edb..2a26e4687 100644
--- a/testcases/pldi2011-testcases/LambdaEval.scala
+++ b/testcases/pldi2011-testcases/LambdaEval.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object LambdaEval {
sealed abstract class Expr
diff --git a/testcases/pldi2011-testcases/PropositionalLogic.scala b/testcases/pldi2011-testcases/PropositionalLogic.scala
index dbdf6e3ee..ef7b0d34a 100644
--- a/testcases/pldi2011-testcases/PropositionalLogic.scala
+++ b/testcases/pldi2011-testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object PropositionalLogic {
diff --git a/testcases/pldi2011-testcases/QuickSort.scala b/testcases/pldi2011-testcases/QuickSort.scala
index db8645ffe..c04560218 100644
--- a/testcases/pldi2011-testcases/QuickSort.scala
+++ b/testcases/pldi2011-testcases/QuickSort.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object QuickSort {
sealed abstract class List
diff --git a/testcases/pldi2011-testcases/RedBlackTree.scala b/testcases/pldi2011-testcases/RedBlackTree.scala
index 0f443af59..aca029fb2 100644
--- a/testcases/pldi2011-testcases/RedBlackTree.scala
+++ b/testcases/pldi2011-testcases/RedBlackTree.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
index c3146a831..7cc45ca3c 100644
--- a/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
+++ b/testcases/pldi2011-testcases/RedBlackTreeDeletion.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
+import leon.Annotations._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/pldi2011-testcases/SemanticsPreservation.scala b/testcases/pldi2011-testcases/SemanticsPreservation.scala
index a5a2a38f9..ece2e608e 100644
--- a/testcases/pldi2011-testcases/SemanticsPreservation.scala
+++ b/testcases/pldi2011-testcases/SemanticsPreservation.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SemanticsPreservation {
diff --git a/testcases/pldi2011-testcases/TreeMap.scala b/testcases/pldi2011-testcases/TreeMap.scala
index fd9bbc038..77318cdd2 100644
--- a/testcases/pldi2011-testcases/TreeMap.scala
+++ b/testcases/pldi2011-testcases/TreeMap.scala
@@ -1,5 +1,5 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
+import leon.Utils._
object TreeMap {
sealed abstract class TreeMap
diff --git a/testcases/sas2011-testcases/AmortizedQueue.scala b/testcases/sas2011-testcases/AmortizedQueue.scala
index db9f1928e..dd5a75f89 100644
--- a/testcases/sas2011-testcases/AmortizedQueue.scala
+++ b/testcases/sas2011-testcases/AmortizedQueue.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AmortizedQueue {
sealed abstract class List
diff --git a/testcases/sas2011-testcases/AssociativeList.scala b/testcases/sas2011-testcases/AssociativeList.scala
index dc56e8fd4..f5a2fc041 100644
--- a/testcases/sas2011-testcases/AssociativeList.scala
+++ b/testcases/sas2011-testcases/AssociativeList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AssociativeList {
sealed abstract class KeyValuePairAbs
diff --git a/testcases/sas2011-testcases/InsertionSort.scala b/testcases/sas2011-testcases/InsertionSort.scala
index c8d4cc707..d2ae67b3b 100644
--- a/testcases/sas2011-testcases/InsertionSort.scala
+++ b/testcases/sas2011-testcases/InsertionSort.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/sas2011-testcases/PropositionalLogic.scala b/testcases/sas2011-testcases/PropositionalLogic.scala
index d95ed58c4..a35c3ef9b 100644
--- a/testcases/sas2011-testcases/PropositionalLogic.scala
+++ b/testcases/sas2011-testcases/PropositionalLogic.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object PropositionalLogic {
diff --git a/testcases/sas2011-testcases/RedBlackTree.scala b/testcases/sas2011-testcases/RedBlackTree.scala
index da5dd22c0..bc2de6ba9 100644
--- a/testcases/sas2011-testcases/RedBlackTree.scala
+++ b/testcases/sas2011-testcases/RedBlackTree.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/sas2011-testcases/SearchLinkedList.scala b/testcases/sas2011-testcases/SearchLinkedList.scala
index d14b9fee6..2c137fd4a 100644
--- a/testcases/sas2011-testcases/SearchLinkedList.scala
+++ b/testcases/sas2011-testcases/SearchLinkedList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SearchLinkedList {
sealed abstract class List
diff --git a/testcases/sas2011-testcases/SumAndMax.scala b/testcases/sas2011-testcases/SumAndMax.scala
index c4265e25b..0aa4ce706 100644
--- a/testcases/sas2011-testcases/SumAndMax.scala
+++ b/testcases/sas2011-testcases/SumAndMax.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SumAndMax {
sealed abstract class List
diff --git a/testcases/vmcai2011-testcases/JustFormulas.scala b/testcases/vmcai2011-testcases/JustFormulas.scala
index fada0552d..bb902f0d5 100644
--- a/testcases/vmcai2011-testcases/JustFormulas.scala
+++ b/testcases/vmcai2011-testcases/JustFormulas.scala
@@ -2,7 +2,7 @@ import scala.collection.immutable.Set
object JustFormulas {
// These are just to provide some "uninterpreted function symbols"
- // Use the option -P:funcheck:tolerant to avoid warnings about it.
+ // Use the option -P:leon:tolerant to avoid warnings about it.
def f1(x: Int) : Int = { throw new Exception("Not implemented") }
def f2(s: Set[Int]) : Set[Int] = { throw new Exception("Not implemented") }
def f3(x: Int) : Set[Int] = { throw new Exception("Not implemented") }
diff --git a/testcases/vmcai2011-testcases/SanityChecks.scala b/testcases/vmcai2011-testcases/SanityChecks.scala
index 2eb68f673..5ee5f3d96 100644
--- a/testcases/vmcai2011-testcases/SanityChecks.scala
+++ b/testcases/vmcai2011-testcases/SanityChecks.scala
@@ -2,7 +2,7 @@ import scala.collection.immutable.Set
object SanityChecks {
// These are just to provide some "uninterpreted function symbols"
- // Use the option -P:funcheck:tolerant to avoid warnings about it.
+ // Use the option -P:leon:tolerant to avoid warnings about it.
def f1(x: Int) : Int = { throw new Exception("Not implemented") }
def f2(s: Set[Int]) : Set[Int] = { throw new Exception("Not implemented") }
def f3(x: Int) : Set[Int] = { throw new Exception("Not implemented") }
diff --git a/testcases/vstte10competition/AmortizedQueue.scala b/testcases/vstte10competition/AmortizedQueue.scala
index 9c049989d..fa9d8f023 100644
--- a/testcases/vstte10competition/AmortizedQueue.scala
+++ b/testcases/vstte10competition/AmortizedQueue.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object AmortizedQueue {
sealed abstract class List
diff --git a/testcases/vstte10competition/Injection.scala b/testcases/vstte10competition/Injection.scala
index 1bb8b3ee2..e20fdcedd 100644
--- a/testcases/vstte10competition/Injection.scala
+++ b/testcases/vstte10competition/Injection.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object Injection {
sealed abstract class List
diff --git a/testcases/vstte10competition/SearchLinkedList.scala b/testcases/vstte10competition/SearchLinkedList.scala
index d14b9fee6..2c137fd4a 100644
--- a/testcases/vstte10competition/SearchLinkedList.scala
+++ b/testcases/vstte10competition/SearchLinkedList.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SearchLinkedList {
sealed abstract class List
diff --git a/testcases/vstte10competition/SumAndMax.scala b/testcases/vstte10competition/SumAndMax.scala
index c4265e25b..0aa4ce706 100644
--- a/testcases/vstte10competition/SumAndMax.scala
+++ b/testcases/vstte10competition/SumAndMax.scala
@@ -1,5 +1,5 @@
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
object SumAndMax {
sealed abstract class List
--
GitLab