From faf7174b2ed5c92322206b22c33dc26761091bd8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 12 Dec 2012 01:33:14 +0100
Subject: [PATCH] most tests are working
---
.../scala/leon/solvers/z3/FairZ3Solver.scala | 1 -
.../scala/leon/verification/AnalysisPhase.scala | 1 -
.../leon/xlang/ImperativeCodeElimination.scala | 2 --
.../verification/xlang/invalid/MyTuple1.scala | 11 -----------
.../verification/xlang/invalid/MyTuple2.scala | 14 --------------
.../verification/xlang/invalid/MyTuple3.scala | 7 -------
.../verification/xlang/valid/MyTuple1.scala | 11 -----------
.../verification/xlang/valid/MyTuple3.scala | 8 --------
.../verification/xlang/valid/MyTuple4.scala | 14 --------------
.../verification/xlang/valid/MyTuple5.scala | 16 ----------------
.../verification/xlang/valid/MyTuple6.scala | 8 --------
.../XLangVerificationRegression.scala | 4 +++-
12 files changed, 3 insertions(+), 94 deletions(-)
delete mode 100644 src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
delete mode 100644 src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
delete mode 100644 src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
delete mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple1.scala
delete mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
delete mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
delete mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
delete mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index bc246e2e6..c9c69511e 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -291,7 +291,6 @@ class FairZ3Solver(context : LeonContext)
val newClauses = unrollingBank.scanForNewTemplates(expression)
for (cl <- newClauses) {
- println("transforming to z3: " + cl)
solver.assertCnstr(z3.mkImplies(guard, toZ3Formula(cl).get))
}
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2785fae3e..d4a2b71b7 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -21,7 +21,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
)
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
- println(program)
val functionsToAnalyse : MutableSet[String] = MutableSet.empty
for(opt <- ctx.options) opt match {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 330e44c13..b926893cd 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -24,7 +24,6 @@ object ImperativeCodeElimination extends TransformationPhase {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
- println("processing fun: " + fd)
parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
@@ -39,7 +38,6 @@ object ImperativeCodeElimination extends TransformationPhase {
private def toFunction(expr: Expr): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
val res = expr match {
case LetVar(id, e, b) => {
- println("in letvar with id: " + id)
val newId = FreshIdentifier(id.name).setType(id.getType)
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
varInScope += id
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
deleted file mode 100644
index f2b06b5b2..000000000
--- a/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object MyTuple1 {
-
- def foo(): Int = {
- val t = (1, true, 3)
- val a1 = t._1
- val a2 = t._2
- val a3 = t._3
- a3
- } ensuring( _ == 1)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
deleted file mode 100644
index 22b62dc75..000000000
--- a/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-object MyTuple2 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t = (B(2), C(B(3)))
- t match {
- case (B(x), C(y)) => x
- }
- } ensuring( _ == 3)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
deleted file mode 100644
index da9f85b16..000000000
--- a/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-object MyTuple3 {
-
- def foo(t: (Int, Int)): (Int, Int) = {
- t
- } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple1.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple1.scala
deleted file mode 100644
index 48383898e..000000000
--- a/src/test/resources/regression/verification/xlang/valid/MyTuple1.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-object MyTuple1 {
-
- def foo(): Int = {
- val t = (1, true, 3)
- val a1 = t._1
- val a2 = t._2
- val a3 = t._3
- a3
- } ensuring( _ == 3)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
deleted file mode 100644
index 2e14c067b..000000000
--- a/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object MyTuple3 {
-
- def foo(): Int = {
- val t = ((2, 3), true)
- t._1._2
- } ensuring( _ == 3)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
deleted file mode 100644
index 6fcfed661..000000000
--- a/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-
-object MyTuple4 {
-
- abstract class A
- case class B(i: Int) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t = (1, (C(B(4)), 2), 3)
- val (a1, (C(B(x)), a2), a3) = t
- x
- } ensuring( _ == 4)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
deleted file mode 100644
index 6a55bc8c9..000000000
--- a/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-object MyTuple1 {
-
- abstract class A
- case class B(t: (Int, Int)) extends A
- case class C(a: A) extends A
-
- def foo(): Int = {
- val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
- t match {
- case (_, (B((x, y)), _), _) => x
- case (_, (C(B((_, x))), _), y) => x
- case (_, _, x) => x
- }
- } ensuring( _ == 5)
-
-}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
deleted file mode 100644
index a54710fbb..000000000
--- a/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-object MyTuple6 {
-
- def foo(t: (Int, Int)): (Int, Int) = {
- require(t._1 > 0 && t._2 > 1)
- t
- } ensuring(res => res._1 > 0 && res._2 > 1)
-
-}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 024641fd9..16973fe53 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -20,10 +20,10 @@ class XLangVerificationRegression extends FunSuite {
private def mkPipeline : Pipeline[List[String],VerificationReport] =
leon.plugin.ExtractionPhase andThen
+ xlang.ArrayTransformation andThen
xlang.EpsilonElimination andThen
xlang.ImperativeCodeElimination andThen
xlang.FunctionClosure andThen
- xlang.ArrayTransformation andThen
leon.verification.AnalysisPhase
private def mkTest(file : File)(block: Output=>Unit) = {
@@ -40,6 +40,8 @@ class XLangVerificationRegression extends FunSuite {
assert(file.exists && file.isFile && file.canRead,
"Benchmark %s is not a readable file".format(displayName))
+ println("testing " + displayName)
+
val ctx = LeonContext(
settings = Settings(
synthesis = false,
--
GitLab