Skip to content
Snippets Groups Projects
Commit 4b5362dd authored by Regis Blanc's avatar Regis Blanc
Browse files

first batch of tests for array mutation

parent 9f64c5f0
No related branches found
No related tags found
No related merge requests found
......@@ -109,8 +109,8 @@ Keys.fork in run := true
lazy val testSettings = Seq(
//Keys.fork := true,
logBuffered := true,
parallelExecution := true
logBuffered := false,
parallelExecution := false
//testForkedParallel := true,
//javaOptions ++= Seq("-Xss64M", "-Xmx4G")
)
......
......@@ -262,7 +262,6 @@ object AntiAliasingPhase extends TransformationPhase {
}
}
def invocEffects(fi: FunctionInvocation): Set[Identifier] = {
if(!effects.isDefinedAt(fi.tfd.fd)) {
println("fi not defined: " + fi)
......@@ -276,7 +275,6 @@ object AntiAliasingPhase extends TransformationPhase {
}.toSet
}
rec()
effects
}
......
import leon.lang._
object ArrayParamMutation1 {
def update(a: Array[BigInt]): Unit = {
require(a.length > 0)
a(0) = 10
}
def f(): BigInt = {
val a = Array.fill(10)(BigInt(0))
update(a)
a(0)
} ensuring(res => res == 10)
}
import leon.lang._
object ArrayParamMutation2 {
def rec(a: Array[BigInt]): BigInt = {
require(a.length > 1 && a(0) >= 0)
if(a(0) == 0)
a(1)
else {
a(0) = a(0) - 1
a(1) = a(1) + a(0)
rec(a)
}
} ensuring(res => a(0) == 0)
}
import leon.lang._
object ArrayParamMutation3 {
def odd(a: Array[BigInt]): Boolean = {
require(a.length > 0 && a(0) >= 0)
if(a(0) == 0) false
else {
a(0) = a(0) - 1
even(a)
}
} ensuring(res => a(0) == 0)
def even(a: Array[BigInt]): Boolean = {
require(a.length > 0 && a(0) >= 0)
if(a(0) == 0) true
else {
a(0) = a(0) - 1
odd(a)
}
} ensuring(res => a(0) == 0)
}
import leon.lang._
object ArrayParamMutation4 {
def multipleArgs(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a2.length > 0)
if(a1(0) == 10)
a2(0) = 13
else
a2(0) = a1(0) + 1
}
def transitiveEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a2.length > 0)
multipleArgs(a1, a2)
} ensuring(_ => a2(0) >= a1(0))
def transitiveReverseEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a2.length > 0)
multipleArgs(a2, a1)
} ensuring(_ => a1(0) >= a2(0))
}
import leon.lang._
object ArrayParamMutation5 {
def mutuallyRec1(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a1(0) > 0 && a2.length > 0)
if(a1(0) == 10) {
()
} else {
mutuallyRec2(a1, a2)
}
} ensuring(res => a1(0) == 10)
def mutuallyRec2(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a2.length > 0 && a1(0) > 0)
a1(0) = 10
mutuallyRec1(a1, a2)
}
}
import leon.lang._
object ArrayParamMutation6 {
def multipleEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a2.length > 0)
a1(0) = 11
a2(0) = 12
} ensuring(_ => a1(0) != a2(0))
def f(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
require(a1.length > 0 && a2.length > 0)
multipleEffects(a1, a2)
} ensuring(_ => a1(0) == 11 && a2(0) == 12)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment