From cc618ebdb1e633566e58bd49caa0cf9a28a33607 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 14 Sep 2015 13:13:51 +0200
Subject: [PATCH] Termination does not need xlang
Remove weird test case (no idea why it worked)
---
.../termination/valid/BinaryTreeImp.scala | 102 ------------------
.../termination/TerminationSuite.scala | 4 +-
2 files changed, 2 insertions(+), 104 deletions(-)
delete mode 100644 src/test/resources/regression/termination/valid/BinaryTreeImp.scala
diff --git a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
deleted file mode 100644
index c758798bf..000000000
--- a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
+++ /dev/null
@@ -1,102 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-import leon.annotation._
-import leon.lang._
-
-object BinaryTree {
-
- sealed abstract class Tree
- case class Leaf() extends Tree
- case class Node(left: Tree, value: Int, right: Tree) extends Tree
-
- sealed abstract class OptionInt
- case class Some(v : Int) extends OptionInt
- case class None() extends OptionInt
-
- def content(t: Tree) : Set[Int] = t match {
- case Leaf() => Set.empty
- case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
-
- def size(t: Tree) : Int = (t match {
- case Leaf() => 0
- case Node(l, v, r) => size(l) + 1 + size(r)
- }) ensuring(_ >= 0)
-
- def binaryTreeProp(t: Tree): Boolean = t match {
- case Leaf() => true
- case Node(left, value, right) => {
- val b1 = left match {
- case Leaf() => true
- case Node(a,b,c) => value >= treeMax(Node(a,b,c))
- }
- val b2 = right match {
- case Leaf() => true
- case Node(a,b,c) => value <= treeMin(Node(a,b,c))
- }
- binaryTreeProp(left) && binaryTreeProp(right) && b1 && b2
- }
- }
-
- def treeMin(tree: Node): Int = {
- require(binaryTreeProp(tree))
- tree match {
- case Node(left, value, _) => left match {
- case Leaf() => value
- case Node(l, v, r) => treeMin(Node(l, v, r))
- }
- }
- } ensuring(content(tree).contains(_))
-
- //def treeMin(tree: Node): Int = {
- // require(binaryTreeProp(tree))
- // val Node(left, value, _) = tree
- // var res = value
- // var tmpLeft = left
- // (while(!tmpLeft.isInstanceOf[Leaf]) {
- // val Node(left, value, _) = tmpLeft
- // res = value
- // tmpLeft = left
- // }) invariant(content(tmpLeft).contains(res))
- // res
- //} ensuring(content(tree).contains(_))
-
- def treeMax(tree: Node): Int = {
- require(binaryTreeProp(tree))
- tree match {
- case Node(_, v, right) => right match {
- case Leaf() => v
- case Node(l, v, r) => treeMax(Node(l, v, r))
- }
- }
- } ensuring(content(tree).contains(_))
-
-
- def search(t: Tree, x: Int): Boolean = {
- require(binaryTreeProp(t))
- t match {
- case Leaf() => false
- case Node(left, value, right) =>
- if(value == x) true
- else if(value < x) search(right, x)
- else search(left, x)
- }
- } ensuring(res => res == content(t).contains(x))
-
- def searchImp(t: Tree, x: Int): Boolean = {
- require(binaryTreeProp(t))
- var res = false
- var t2: Tree = t
- (while(!t2.isInstanceOf[Leaf]) {
- val Node(left, value, right) = t2
- if(value == x)
- res = true
- else if(value < x)
- t2 = right
- else
- t2 = left
- })
- res
- } ensuring(res => res == content(t).contains(x))
-
-}
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index be0e1cdfd..09ad300b6 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -18,8 +18,8 @@ class TerminationSuite extends LeonRegressionSuite {
private case class Output(report : TerminationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],TerminationReport] =
- leon.frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase(desugarXLang = true) andThen
+ leon.frontends.scalac.ExtractionPhase andThen
+ new leon.utils.PreprocessingPhase andThen
leon.termination.TerminationPhase
private def mkTest(file : File, leonOptions: Seq[LeonOption[Any]], forError: Boolean)(block: Output=>Unit) = {
--
GitLab