-
Etienne Kneuss authored
unit, integration, and regression tests can now share code as they are compiled together. Unit tests are now in package leon.unit and shared code lives in leon.test.
Etienne Kneuss authoredunit, integration, and regression tests can now share code as they are compiled together. Unit tests are now in package leon.unit and shared code lives in leon.test.
Array6.scala 251 B
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
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)
}
}