Skip to content
Snippets Groups Projects
Commit 54e1f4ae authored by Régis Blanc's avatar Régis Blanc
Browse files

add regression to the top level and adapt run-tests script

parent 1bcf168b
No related branches found
No related tags found
No related merge requests found
Showing
with 238 additions and 0 deletions
import leon.Utils._
object Epsilon5 {
def fooWrong(x: Int, y: Int): Int = {
epsilon((z: Int) => z >= x && z <= y)
} ensuring(_ > x)
}
import leon.Utils._
object Epsilon6 {
def greaterWrong(x: Int): Int = {
epsilon((y: Int) => y >= x)
} ensuring(_ > x)
}
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(_ == 3)
}
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)
}
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)
}
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)
}
object MyTuple3 {
def foo(t: (Int, Int)): (Int, Int) = {
t
} ensuring(res => res._1 > 0 && res._2 > 1)
}
object Unit1 {
def foo(u: Unit): Unit = ({
u
}) ensuring(_ != ())
}
object Array1 {
def foo(): Int = {
val a = Array.fill(5)(0)
a(2) = 3
a(2)
} ensuring(_ == 3)
}
object Array10 {
def foo(a: Array[Int]): Int = {
require(a.length > 0)
val b = a.clone
b(0)
} ensuring(res => res == a(0))
}
object Array2 {
def foo(): Int = {
val a = Array.fill(5)(0)
a(2) = 3
a.length
} ensuring(_ == 5)
}
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)
}
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
}
}
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)
}
}
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)
}
}
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))
}
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)
}
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)
}
}
object Assign1 {
def foo(): Int = {
var a = 0
val tmp = a + 1
a = a + 2
a = a + tmp
a = a + 4
a
} ensuring(_ == 7)
}
import leon.Utils._
object Epsilon1 {
def greater(x: Int): Int = {
epsilon((y: Int) => y > x)
} ensuring(_ >= x)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment