From 67dc991d669980493beb5ad098b6294e0094f96b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 11 Dec 2012 23:24:41 +0100
Subject: [PATCH] adding new regressions tests
---
src/main/scala/leon/Settings.scala | 2 +-
.../scala/leon/solvers/z3/FairZ3Solver.scala | 1 +
.../leon/verification/AnalysisPhase.scala | 1 +
.../leon/xlang/ArrayTransformation.scala | 4 +-
.../scala/leon/xlang/FunctionClosure.scala | 10 +-
.../xlang/ImperativeCodeElimination.scala | 5 +
src/main/scala/leon/xlang/Trees.scala | 108 +++++++++++-------
.../verification/xlang/invalid/Array1.scala | 9 ++
.../verification/xlang/invalid/Array2.scala | 9 ++
.../verification/xlang/invalid/Array3.scala | 16 +++
.../verification/xlang/invalid/Array4.scala | 9 ++
.../verification/xlang/invalid/Array5.scala | 10 ++
.../verification/xlang/invalid/Epsilon1.scala | 12 ++
.../verification/xlang/invalid/Epsilon2.scala | 11 ++
.../verification/xlang/invalid/Epsilon3.scala | 9 ++
.../verification/xlang/invalid/Epsilon4.scala | 27 +++++
.../verification/xlang/invalid/Epsilon5.scala | 9 ++
.../verification/xlang/invalid/Epsilon6.scala | 9 ++
.../verification/xlang/invalid/IfExpr2.scala | 14 +++
.../verification/xlang/invalid/MyTuple1.scala | 11 ++
.../verification/xlang/invalid/MyTuple2.scala | 14 +++
.../verification/xlang/invalid/MyTuple3.scala | 7 ++
.../verification/xlang/invalid/Unit1.scala | 7 ++
.../verification/xlang/valid/Array1.scala | 9 ++
.../verification/xlang/valid/Array10.scala | 9 ++
.../verification/xlang/valid/Array2.scala | 9 ++
.../verification/xlang/valid/Array3.scala | 16 +++
.../verification/xlang/valid/Array4.scala | 15 +++
.../verification/xlang/valid/Array5.scala | 20 ++++
.../verification/xlang/valid/Array6.scala | 15 +++
.../verification/xlang/valid/Array7.scala | 17 +++
.../verification/xlang/valid/Array8.scala | 8 ++
.../verification/xlang/valid/Array9.scala | 15 +++
.../verification/xlang/valid/Assign1.scala | 12 ++
.../verification/xlang/valid/Epsilon1.scala | 9 ++
.../verification/xlang/valid/Epsilon2.scala | 13 +++
.../verification/xlang/valid/Epsilon3.scala | 9 ++
.../verification/xlang/valid/Epsilon4.scala | 32 ++++++
.../verification/xlang/valid/Epsilon5.scala | 9 ++
.../verification/xlang/valid/Field1.scala | 11 ++
.../verification/xlang/valid/Field2.scala | 11 ++
.../verification/xlang/valid/IfExpr1.scala | 13 +++
.../verification/xlang/valid/IfExpr2.scala | 14 +++
.../verification/xlang/valid/IfExpr3.scala | 19 +++
.../verification/xlang/valid/IfExpr4.scala | 18 +++
.../xlang/valid/InstanceOf1.scala | 18 +++
.../verification/xlang/valid/MyTuple3.scala | 8 ++
.../verification/xlang/valid/MyTuple4.scala | 14 +++
.../verification/xlang/valid/MyTuple5.scala | 16 +++
.../verification/xlang/valid/MyTuple6.scala | 8 ++
.../verification/xlang/valid/Nested1.scala | 15 +++
.../verification/xlang/valid/Nested10.scala | 14 +++
.../verification/xlang/valid/Nested11.scala | 14 +++
.../verification/xlang/valid/Nested12.scala | 17 +++
.../verification/xlang/valid/Nested13.scala | 21 ++++
.../verification/xlang/valid/Nested14.scala | 11 ++
.../verification/xlang/valid/Nested2.scala | 13 +++
.../verification/xlang/valid/Nested3.scala | 15 +++
.../verification/xlang/valid/Nested4.scala | 19 +++
.../verification/xlang/valid/Nested5.scala | 12 ++
.../verification/xlang/valid/Nested6.scala | 14 +++
.../verification/xlang/valid/Nested7.scala | 19 +++
.../verification/xlang/valid/Nested8.scala | 43 +++++++
.../verification/xlang/valid/Nested9.scala | 23 ++++
.../verification/xlang/valid/NestedVar.scala | 17 +++
.../verification/xlang/valid/Unit1.scala | 7 ++
.../verification/xlang/valid/Unit2.scala | 7 ++
.../verification/xlang/valid/While1.scala | 13 +++
.../verification/xlang/valid/While2.scala | 13 +++
.../verification/xlang/valid/While3.scala | 13 +++
70 files changed, 953 insertions(+), 48 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Array1.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Array2.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Array3.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Array4.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Array5.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Unit1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array10.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array3.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array4.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array5.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array6.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array7.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array8.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Array9.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Assign1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Field1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Field2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested10.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested11.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested12.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested13.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested14.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested3.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested4.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested5.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested6.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested7.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested8.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested9.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/NestedVar.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Unit1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Unit2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/While1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/While2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/While3.scala
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 9aa0c57ac..3aba078e9 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -5,7 +5,7 @@ package leon
object Settings {
lazy val reporter: Reporter = new DefaultReporter
- var showIDs: Boolean = false
+ var showIDs: Boolean = true
var silentlyTolerateNonPureBodies: Boolean = false
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index c9c69511e..bc246e2e6 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -291,6 +291,7 @@ 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 d4a2b71b7..2785fae3e 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -21,6 +21,7 @@ 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/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 1d7a20dcf..880e870f5 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -14,8 +14,11 @@ object ArrayTransformation extends TransformationPhase {
val name = "Array Transformation"
val description = "Add bound checking for array access and remove array update with side effect"
+ private var id2FreshId = Map[Identifier, Identifier]()
+
def apply(ctx: LeonContext, pgm: Program): Program = {
+ id2FreshId = Map()
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
id2FreshId = Map()
@@ -26,7 +29,6 @@ object ArrayTransformation extends TransformationPhase {
pgm
}
- private var id2FreshId = Map[Identifier, Identifier]()
def transform(expr: Expr): Expr = expr match {
case sel@ArraySelect(a, i) => {
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index 6c5000849..47e0cbeed 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/src/main/scala/leon/xlang/FunctionClosure.scala
@@ -21,14 +21,20 @@ object FunctionClosure extends TransformationPhase{
private var topLevelFuns: Set[FunDef] = Set()
def apply(ctx: LeonContext, program: Program): Program = {
- newFunDefs = Map()
+
+ pathConstraints = Nil
+ enclosingLets = Nil
+ newFunDefs = Map()
+ topLevelFuns = Set()
+
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
pathConstraints = fd.precondition.toList
fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet, Map(), Map()))
})
val Program(id, ObjectDef(objId, defs, invariants)) = program
- Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
+ val res = Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
+ res
}
private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index c66a70949..330e44c13 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -19,8 +19,12 @@ object ImperativeCodeElimination extends TransformationPhase {
private var parent: FunDef = null //the enclosing fundef
def apply(ctx: LeonContext, pgm: Program): Program = {
+ varInScope = Set()
+ parent = null
+
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))
@@ -35,6 +39,7 @@ 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/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 8995aba73..31c717784 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -260,39 +260,51 @@ object Trees {
(fd.precondition, fd.postcondition) match {
case (None, None) =>
Some((Seq(b, body), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ LetDef(fd, as(1))
}))
case (Some(pre), None) =>
Some((Seq(b, body, pre), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- nfd.precondition = Some(as(2))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //nfd.precondition = Some(as(2))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ fd.precondition = Some(as(2))
+ LetDef(fd, as(1))
}))
case (None, Some(post)) =>
Some((Seq(b, body, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- nfd.postcondition = Some(as(2))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //nfd.postcondition = Some(as(2))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ fd.postcondition = Some(as(2))
+ LetDef(fd, as(1))
}))
case (Some(pre), Some(post)) =>
Some((Seq(b, body, pre, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- nfd.precondition = Some(as(2))
- nfd.postcondition = Some(as(3))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //nfd.precondition = Some(as(2))
+ //nfd.postcondition = Some(as(3))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ fd.precondition = Some(as(2))
+ fd.postcondition = Some(as(3))
+ LetDef(fd, as(1))
}))
}
@@ -300,35 +312,43 @@ object Trees {
(fd.precondition, fd.postcondition) match {
case (None, None) =>
Some((Seq(body), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //LetDef(nfd, as(0))
+ LetDef(fd, as(0))
}))
case (Some(pre), None) =>
Some((Seq(body, pre), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.precondition = Some(as(1))
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.precondition = Some(as(1))
+ //LetDef(nfd, as(0))
+ fd.precondition = Some(as(1))
+ LetDef(fd, as(0))
}))
case (None, Some(post)) =>
Some((Seq(body, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.postcondition = Some(as(1))
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.postcondition = Some(as(1))
+ //LetDef(nfd, as(0))
+ fd.postcondition = Some(as(1))
+ LetDef(fd, as(0))
}))
case (Some(pre), Some(post)) =>
Some((Seq(body, pre, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.precondition = Some(as(1))
- nfd.postcondition = Some(as(2))
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.precondition = Some(as(1))
+ //nfd.postcondition = Some(as(2))
+ //LetDef(nfd, as(0))
+ fd.precondition = Some(as(1))
+ fd.postcondition = Some(as(2))
+ LetDef(fd, as(0))
}))
}
}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array1.scala b/src/test/resources/regression/verification/xlang/invalid/Array1.scala
new file mode 100644
index 000000000..a8451250c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array2.scala b/src/test/resources/regression/verification/xlang/invalid/Array2.scala
new file mode 100644
index 000000000..54ab5e3c2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 4)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array3.scala b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
new file mode 100644
index 000000000..0c1bb76fd
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i <= a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array4.scala b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
new file mode 100644
index 000000000..5b5e74061
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
new file mode 100644
index 000000000..ecb003349
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
@@ -0,0 +1,10 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2)
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
new file mode 100644
index 000000000..c3c0a48be
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
@@ -0,0 +1,12 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand2(x: Int): Int = epsilon((y: Int) => true)
+
+ //this should not hold
+ def property2(x: Int): Boolean = {
+ rand2(x) == rand2(x+1)
+ } holds
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
new file mode 100644
index 000000000..20699fc42
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand3(x: Int): Int = epsilon((y: Int) => x == x)
+
+ //this should not hold
+ def property3(x: Int): Boolean = {
+ rand3(x) == rand3(x+1)
+ } holds
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
new file mode 100644
index 000000000..5ff47b6d6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+ def posWrong(): Int = {
+ epsilon((y: Int) => y >= 0)
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
new file mode 100644
index 000000000..6619e59d6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
@@ -0,0 +1,27 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ sealed abstract class MyList
+ case class MyCons(head: Int, tail: MyList) extends MyList
+ case class MyNil() extends MyList
+
+ def size(lst: MyList): Int = (lst match {
+ case MyNil() => 0
+ case MyCons(_, xs) => 1 + size(xs)
+ })
+
+ def toSet(lst: MyList): Set[Int] = lst match {
+ case MyCons(x, xs) => toSet(xs) ++ Set(x)
+ case MyNil() => Set[Int]()
+ }
+
+ def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+ val elem = epsilon((x : Int) => set contains x)
+ MyCons(elem, toList(set -- Set[Int](elem)))
+ }
+
+
+ def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
+ //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
new file mode 100644
index 000000000..b96fa7564
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+ def fooWrong(x: Int, y: Int): Int = {
+ epsilon((z: Int) => z >= x && z <= y)
+ } ensuring(_ > x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
new file mode 100644
index 000000000..bc5aca78c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon6 {
+
+ def greaterWrong(x: Int): Int = {
+ epsilon((y: Int) => y >= x)
+ } ensuring(_ > x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala b/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
new file mode 100644
index 000000000..1284904b5
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
@@ -0,0 +1,14 @@
+object IfExpr2 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if(a < b) {
+ a = a + 3
+ b = b + 2
+ a = a + b
+ }
+ a
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
new file mode 100644
index 000000000..f2b06b5b2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
@@ -0,0 +1,11 @@
+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
new file mode 100644
index 000000000..22b62dc75
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
@@ -0,0 +1,14 @@
+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
new file mode 100644
index 000000000..da9f85b16
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
@@ -0,0 +1,7 @@
+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/invalid/Unit1.scala b/src/test/resources/regression/verification/xlang/invalid/Unit1.scala
new file mode 100644
index 000000000..789a8f058
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(u: Unit): Unit = ({
+ u
+ }) ensuring(_ != ())
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array1.scala b/src/test/resources/regression/verification/xlang/valid/Array1.scala
new file mode 100644
index 000000000..3815f0344
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array10.scala b/src/test/resources/regression/verification/xlang/valid/Array10.scala
new file mode 100644
index 000000000..ebb60ad6e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array10.scala
@@ -0,0 +1,9 @@
+object Array10 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val b = a.clone
+ b(0)
+ } ensuring(res => res == a(0))
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array2.scala b/src/test/resources/regression/verification/xlang/valid/Array2.scala
new file mode 100644
index 000000000..4f149a930
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array3.scala b/src/test/resources/regression/verification/xlang/valid/Array3.scala
new file mode 100644
index 000000000..bbb1845b8
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array4.scala b/src/test/resources/regression/verification/xlang/valid/Array4.scala
new file mode 100644
index 000000000..fd76e02fa
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array4.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array5.scala b/src/test/resources/regression/verification/xlang/valid/Array5.scala
new file mode 100644
index 000000000..14bed6eff
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array5.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/xlang/valid/Array6.scala
new file mode 100644
index 000000000..bdd6b0c5d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array6.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array6 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2 && a(2) == 5)
+ a(2)
+ } ensuring(_ == 5)
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array7.scala b/src/test/resources/regression/verification/xlang/valid/Array7.scala
new file mode 100644
index 000000000..55bbbb729
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array7.scala
@@ -0,0 +1,17 @@
+import leon.Utils._
+
+object Array7 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length > 0)
+ val a2 = Array.fill(a.length)(0)
+ var i = 0
+ (while(i < a.length) {
+ a2(i) = a(i)
+ i = i + 1
+ }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true))
+ a2
+ } ensuring(_(0) == a(0))
+
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array8.scala b/src/test/resources/regression/verification/xlang/valid/Array8.scala
new file mode 100644
index 000000000..270b18122
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array8.scala
@@ -0,0 +1,8 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length >= 2)
+ a.updated(1, 3)
+ } ensuring(res => res.length == a.length && res(1) == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array9.scala b/src/test/resources/regression/verification/xlang/valid/Array9.scala
new file mode 100644
index 000000000..f49333236
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array9.scala
@@ -0,0 +1,15 @@
+object Array9 {
+
+ def foo(i: Int): Array[Int] = {
+ require(i > 0)
+ val a = Array.fill(i)(0)
+ a
+ } ensuring(res => res.length == i)
+
+ def bar(i: Int): Int = {
+ require(i > 0)
+ val b = foo(i)
+ b(0)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Assign1.scala b/src/test/resources/regression/verification/xlang/valid/Assign1.scala
new file mode 100644
index 000000000..0506c6afb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Assign1.scala
@@ -0,0 +1,12 @@
+object Assign1 {
+
+ def foo(): Int = {
+ var a = 0
+ val tmp = a + 1
+ a = a + 2
+ a = a + tmp
+ a = a + 4
+ a
+ } ensuring(_ == 7)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
new file mode 100644
index 000000000..2ae7201dd
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def greater(x: Int): Int = {
+ epsilon((y: Int) => y > x)
+ } ensuring(_ >= x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
new file mode 100644
index 000000000..36e5268e2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand(): Int = epsilon((x: Int) => true)
+
+ //this should hold, that is the expected semantic of our epsilon
+ def property1(): Boolean = {
+ rand() == rand()
+ } holds
+
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
new file mode 100644
index 000000000..f652016d2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+ def pos(): Int = {
+ epsilon((y: Int) => y > 0)
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
new file mode 100644
index 000000000..174042863
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
@@ -0,0 +1,32 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ sealed abstract class MyList
+ case class MyCons(head: Int, tail: MyList) extends MyList
+ case class MyNil() extends MyList
+
+ def size(lst: MyList): Int = (lst match {
+ case MyNil() => 0
+ case MyCons(_, xs) => 1 + size(xs)
+ })
+
+ def toSet(lst: MyList): Set[Int] = lst match {
+ case MyCons(x, xs) => toSet(xs) ++ Set(x)
+ case MyNil() => Set[Int]()
+ }
+
+ def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+ val elem = epsilon((x : Int) => set contains x)
+ MyCons(elem, toList(set -- Set[Int](elem)))
+ }
+
+ //timeout, but this probably means that it is valid as expected
+ //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+ def propertyBase(lst: MyList): Boolean = ({
+ require(lst match { case MyNil() => true case _ => false})
+ size(toList(toSet(lst))) <= size(lst)
+ }) holds
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
new file mode 100644
index 000000000..0427cf086
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+ def foo(x: Int, y: Int): Int = {
+ epsilon((z: Int) => z > x && z < y)
+ } ensuring(_ >= x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Field1.scala b/src/test/resources/regression/verification/xlang/valid/Field1.scala
new file mode 100644
index 000000000..116557ab7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Field1.scala
@@ -0,0 +1,11 @@
+object Field1 {
+
+ abstract sealed class A
+ case class B(size: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.size
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Field2.scala b/src/test/resources/regression/verification/xlang/valid/Field2.scala
new file mode 100644
index 000000000..9a9661023
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Field2.scala
@@ -0,0 +1,11 @@
+object Field2 {
+
+ abstract sealed class A
+ case class B(length: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.length
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
new file mode 100644
index 000000000..82db13d52
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
@@ -0,0 +1,13 @@
+object IfExpr1 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if({a = a + 1; a != b})
+ a = a + 3
+ else
+ b = a + b
+ a
+ } ensuring(_ == 2)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
new file mode 100644
index 000000000..7a681bc72
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
@@ -0,0 +1,14 @@
+object IfExpr2 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if(a < b) {
+ a = a + 3
+ b = b + 2
+ a = a + b
+ }
+ a
+ } ensuring(_ == 8)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
new file mode 100644
index 000000000..86d4e494a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
@@ -0,0 +1,19 @@
+object IfExpr1 {
+
+ def foo(a: Int): Int = {
+
+ if(a > 0) {
+ var a = 1
+ var b = 2
+ a = 3
+ a + b
+ } else {
+ 5
+ //var a = 3
+ //var b = 1
+ //b = b + 1
+ //a + b
+ }
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
new file mode 100644
index 000000000..94b99fde3
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
@@ -0,0 +1,18 @@
+object IfExpr4 {
+
+ def foo(a: Int): Int = {
+
+ if(a > 0) {
+ var a = 1
+ var b = 2
+ a = 3
+ a + b
+ } else {
+ var a = 3
+ var b = 1
+ b = b + 1
+ a + b
+ }
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala b/src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala
new file mode 100644
index 000000000..1c52338bb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala
@@ -0,0 +1,18 @@
+object InstanceOf1 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(i: Int) extends A
+
+ def foo(): Int = {
+ require(C(3).isInstanceOf[C])
+ val b: A = B(2)
+ if(b.isInstanceOf[B])
+ 0
+ else
+ -1
+ } ensuring(_ == 0)
+
+ def bar(): Int = foo()
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
new file mode 100644
index 000000000..2e14c067b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
@@ -0,0 +1,8 @@
+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
new file mode 100644
index 000000000..6fcfed661
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
@@ -0,0 +1,14 @@
+
+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
new file mode 100644
index 000000000..6a55bc8c9
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
@@ -0,0 +1,16 @@
+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
new file mode 100644
index 000000000..a54710fbb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
@@ -0,0 +1,8 @@
+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/resources/regression/verification/xlang/valid/Nested1.scala b/src/test/resources/regression/verification/xlang/valid/Nested1.scala
new file mode 100644
index 000000000..7745f794f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested1.scala
@@ -0,0 +1,15 @@
+object Nested1 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = i + j + n
+ def rec2(j: Int) = {
+ def rec3(k: Int) = k + j + i
+ rec3(5)
+ }
+ rec2(2)
+ } ensuring(i + 7 == _)
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested10.scala b/src/test/resources/regression/verification/xlang/valid/Nested10.scala
new file mode 100644
index 000000000..b3c4f8653
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested10.scala
@@ -0,0 +1,14 @@
+object Nested10 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = {
+ i + j + n
+ }
+ def rec2(j: Int) = {
+ rec1(j)
+ }
+ rec2(2)
+ } ensuring(i + 4 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested11.scala b/src/test/resources/regression/verification/xlang/valid/Nested11.scala
new file mode 100644
index 000000000..0316fc5f2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested11.scala
@@ -0,0 +1,14 @@
+object Nested11 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(j: Int) = b match {
+ case B(b) => i + j + b
+ }
+ rec1(2)
+ } ensuring(i + 5 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested12.scala b/src/test/resources/regression/verification/xlang/valid/Nested12.scala
new file mode 100644
index 000000000..05ac1569f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested12.scala
@@ -0,0 +1,17 @@
+object Nested12 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(a: A, j: Int, j2: Int) = a match {
+ case B(b) => i + j + j2 + b
+ }
+ def rec2(a: A, k: Int) = a match {
+ case B(b) => rec1(a, b, k)
+ }
+ rec2(b, 2)
+ } ensuring(i + 8 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested13.scala b/src/test/resources/regression/verification/xlang/valid/Nested13.scala
new file mode 100644
index 000000000..ccb742494
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested13.scala
@@ -0,0 +1,21 @@
+object Nested13 {
+
+ abstract class D
+ case class E(e: Int) extends D
+ case class F(d: D, f: Int) extends D
+
+ def foo(a : Int): Int = {
+
+ def rec1(d: D, j: Int): Int = d match {
+ case E(e) => j + e + a
+ case F(dNext, f) => f + rec1(dNext, j)
+ }
+
+ def rec2(d: D, i : Int) : Int = d match {
+ case E(e) => e
+ case F(dNext, f) => rec1(d, i)
+ }
+
+ rec2(F(E(2), 3), 0)
+ } ensuring(a + 5 == _)
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested14.scala b/src/test/resources/regression/verification/xlang/valid/Nested14.scala
new file mode 100644
index 000000000..9a79a4f6e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested14.scala
@@ -0,0 +1,11 @@
+object Nested14 {
+
+ def foo(i: Int): Int = {
+ def rec1(j: Int): Int = {
+ def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
+ rec2(j)
+ }
+ rec1(3)
+ } ensuring(0 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested2.scala b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
new file mode 100644
index 000000000..cc7220b02
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
@@ -0,0 +1,13 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested3.scala b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
new file mode 100644
index 000000000..be6e6d04a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
@@ -0,0 +1,15 @@
+object Nested3 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c
+ e
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested4.scala b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
new file mode 100644
index 000000000..ea1e6066c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
@@ -0,0 +1,19 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ e
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested5.scala b/src/test/resources/regression/verification/xlang/valid/Nested5.scala
new file mode 100644
index 000000000..6ba128f41
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested5.scala
@@ -0,0 +1,12 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
new file mode 100644
index 000000000..1c0220c04
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
@@ -0,0 +1,14 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(prop(a, b) && a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+ def prop(x: Int, y: Int): Boolean = x + y > 0
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
new file mode 100644
index 000000000..62f5a567f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
@@ -0,0 +1,19 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c + bar(a) + bar(b) + bar(c)
+ }
+ rec1(2) + bar(a)
+ } ensuring(_ > 0)
+
+
+ def bar(x: Int): Int = {
+ require(x >= 0)
+ x
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
new file mode 100644
index 000000000..e8a05e40e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+
+object Nested8 {
+
+ def foo(a: Int): Int = {
+ require(a > 0)
+
+ def bar(b: Int): Int = {
+ if(a < b) {
+ def rec(c: Int): Int = {
+ require(c > 0)
+ c + b
+ } ensuring(_ > 0)
+ rec(2)
+ } else 3
+ }
+ bar(1)
+ } ensuring(_ > 0)
+
+ /*
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+ */
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
new file mode 100644
index 000000000..3344a2c79
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
@@ -0,0 +1,23 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ def rec2(f: Int): Int = {
+ require(f >= c)
+ f + e
+ } ensuring(_ > 0)
+ rec2(c+1)
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedVar.scala b/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
new file mode 100644
index 000000000..a26b7312b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
@@ -0,0 +1,17 @@
+object NestedVar {
+
+ def foo(): Int = {
+ val a = 3
+ def rec(x: Int): Int = {
+ var b = 3
+ var c = 3
+ if(x > 0)
+ b = 2
+ else
+ c = 2
+ c+b
+ }
+ rec(a)
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Unit1.scala b/src/test/resources/regression/verification/xlang/valid/Unit1.scala
new file mode 100644
index 000000000..a7b890d76
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(): Unit = ({
+ ()
+ }) ensuring(_ == ())
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Unit2.scala b/src/test/resources/regression/verification/xlang/valid/Unit2.scala
new file mode 100644
index 000000000..ac659589a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Unit2.scala
@@ -0,0 +1,7 @@
+object Unit2 {
+
+ def foo(u: Unit): Unit = {
+ u
+ } ensuring(_ == ())
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/While1.scala b/src/test/resources/regression/verification/xlang/valid/While1.scala
new file mode 100644
index 000000000..0d868b399
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/While1.scala
@@ -0,0 +1,13 @@
+object While1 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while(i < 10) {
+ a = a + 1
+ i = i + 1
+ }
+ a
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/While2.scala b/src/test/resources/regression/verification/xlang/valid/While2.scala
new file mode 100644
index 000000000..e841ed40e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/While2.scala
@@ -0,0 +1,13 @@
+object While1 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while(i < 10) {
+ a = a + i
+ i = i + 1
+ }
+ a
+ } ensuring(_ == 45)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/While3.scala b/src/test/resources/regression/verification/xlang/valid/While3.scala
new file mode 100644
index 000000000..da85d5dfa
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/While3.scala
@@ -0,0 +1,13 @@
+object While3 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while({i = i+2; i <= 10}) {
+ a = a + i
+ i = i - 1
+ }
+ a
+ } ensuring(_ == 54)
+
+}
--
GitLab