diff --git a/.gitignore b/.gitignore
index df8c680efb2df4ec5850d58b035038c36afacf36..bfbd461b232f026844f5d7d6fd2b5fb7647fa941 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@ project/boot
project/build
project/target
target
+/leon
diff --git a/mytest/Add.scala b/mytest/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d125e3c72f29d96fdaa7176756efe11ca36b98a
--- /dev/null
+++ b/mytest/Add.scala
@@ -0,0 +1,25 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object Add {
+
+ def add(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+}
diff --git a/mytest/BinarySearch.scala b/mytest/BinarySearch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92d4cf0667fe0175b80ae0da34679e991efcc633
--- /dev/null
+++ b/mytest/BinarySearch.scala
@@ -0,0 +1,73 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object BinarySearch {
+
+ def binarySearch(a: Map[Int, Int], size: Int, key: Int): Int = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, 0, size - 1))
+ var low = 0
+ var high = size - 1
+ var res = -1
+
+ (while(low <= high && res == -1) {
+ val i = (high + low) / 2
+ val v = a(i)
+
+ if(v == key)
+ res = i
+
+ if(v > key)
+ high = i - 1
+ else if(v < key)
+ low = i + 1
+ }) invariant(0 <= low && low <= high + 1 && high < size && (if(res >= 0) a(res) == key else (!occurs(a, 0, low, key) && !occurs(a, high + 1, size, key))))
+ res
+ }) ensuring(res => res >= -1 && res < size && (if(res >= 0) a(res) == key else !occurs(a, 0, size, key)))
+
+
+ def occurs(a: Map[Int, Int], from: Int, to: Int, key: Int): Boolean = {
+ require(isArray(a, to) && to < 5 && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+}
diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index f1f99bc2de807445955ac4ed106fb79fa16bd7d3..4e274e2707b0cff262e712ab4b78b53eee0db990 100644
--- a/mytest/Bubble.scala
+++ b/mytest/Bubble.scala
@@ -1,9 +1,11 @@
import leon.Utils._
+/* The calculus of Computation textbook */
+
object Bubble {
def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size <= 5 && isArray(a, size))
+ require(size < 5 && isArray(a, size))
var i = size - 1
var j = 0
var sortedArray = a
@@ -17,15 +19,18 @@ object Bubble {
}
j = j + 1
}) invariant(
+ j >= 0 &&
j <= i &&
+ i < size &&
isArray(sortedArray, size) &&
partitioned(sortedArray, size, 0, i, i+1, size-1) &&
- partitioned(sortedArray, size, 0, j-1, j, j) &&
- sorted(sortedArray, size, i, size-1)
+ sorted(sortedArray, size, i, size-1) &&
+ partitioned(sortedArray, size, 0, j-1, j, j)
)
i = i - 1
}) invariant(
i >= 0 &&
+ i < size &&
isArray(sortedArray, size) &&
partitioned(sortedArray, size, 0, i, i+1, size-1) &&
sorted(sortedArray, size, i, size-1)
@@ -37,29 +42,81 @@ object Bubble {
require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
var k = l
var isSorted = true
- while(k <= u) {
+ (while(k < u) {
if(a(k) > a(k+1))
isSorted = false
k = k + 1
- }
+ }) invariant(k <= u && k >= l)
isSorted
}
+ /*
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+ */
+ /*
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+ */
+
def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
- require(l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && isArray(a, size) && size < 5)
- 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 && j+1 <= u2)
- i = i + 1
- }) invariant(i >= l1 && i+1 <= u1)
- isPartitionned
+ require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ 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
+ }
}
def isArray(a: Map[Int, Int], size: Int): Boolean = {
diff --git a/mytest/BubbleFun.scala b/mytest/BubbleFun.scala
index a28ae6540419587e622f63698f9f404f0c59792f..5962eea28e93cbd3d496ae9c7dd92af3a1297d15 100644
--- a/mytest/BubbleFun.scala
+++ b/mytest/BubbleFun.scala
@@ -2,82 +2,127 @@ object BubbleFun {
// --------------------- sort ----------------------
- def sort(a: Map[Int,Int], size: Int): Map[Int,Int] = {
+ def sort(a: Map[Int,Int], size: Int): Map[Int,Int] = ({
+ require(isArray(a, size) && size < 5)
+
val i = size - 1
- val t = sortWhile(0, a, i, a, i, size, a)
+ val t = sortWhile(0, a, i, size)
t._2
- }
+ }) ensuring(res => isArray(res, size) && sorted(res, size, 0, size-1) /*&& content(res, size) == content(a, size)*/)
+
+ def sortWhile(j: Int, sortedArray: Map[Int,Int], i: Int, size: Int) : (Int, Map[Int,Int], Int) = ({
+ require(i >= 0 && i < size && isArray(sortedArray, size) && size < 5 &&
+ sorted(sortedArray, size, i, size - 1) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1))
+
+ if (i > 0) {
+ val t = sortNestedWhile(sortedArray, 0, i, size)
+ sortWhile(t._2, t._1, i - 1, size)
+ } else (j, sortedArray, i)
+ }) ensuring(res => isArray(res._2, size) &&
+ sorted(res._2, size, res._3, size - 1) &&
+ partitioned(res._2, size, 0, res._3, res._3+1, size-1) &&
+ res._3 >= 0 && res._3 <= 0 /*&& content(res._2, size) == content(sortedArray, size)*/
+ )
+
+
+ def sortNestedWhile(sortedArray: Map[Int,Int], j: Int, i: Int, size: Int) : (Map[Int,Int], Int) = ({
+ require(j >= 0 && j <= i && i < size && isArray(sortedArray, size) && size < 5 &&
+ sorted(sortedArray, size, i, size - 1) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ partitioned(sortedArray, size, 0, j-1, j, j))
+ if(j < i) {
+ val newSortedArray =
+ if(sortedArray(j) > sortedArray(j + 1))
+ sortedArray.updated(j, sortedArray(j + 1)).updated(j+1, sortedArray(j))
+ else
+ sortedArray
+ sortNestedWhile(newSortedArray, j + 1, i, size)
+ } else (sortedArray, j)
+ }) ensuring(res => isArray(res._1, size) &&
+ sorted(res._1, size, i, size - 1) &&
+ partitioned(res._1, size, 0, i, i+1, size-1) &&
+ partitioned(res._1, size, 0, res._2-1, res._2, res._2) &&
+ res._2 >= i && res._2 >= 0 && res._2 <= i /*&& content(res._1, size) == content(sortedArray, size)*/)
+
+
+ //some intermediate results
+ def lemma1(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
+ val t = sortNestedWhile(a, 0, i, size)
+ val newJ = t._2
+ i == newJ
+ }) ensuring(_ == true)
+ def lemma2(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
+ val t = sortNestedWhile(a, 0, i, size)
+ val newA = t._1
+ val newJ = t._2
+ partitioned(newA, size, 0, i-1, i, i)
+ }) ensuring(_ == true)
+ def lemma3(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(partitioned(a, size, 0, i, i+1, size-1) && partitioned(a, size, 0, i-1, i, i) && isArray(a, size) && size < 5 && i >= 0 && i < size)
+ partitioned(a, size, 0, i-1, i, size-1)
+ }) ensuring(_ == true)
+ def lemma4(a: Map[Int, Int], size: Int, i: Int): Boolean = ({
+ require(isArray(a, size) && size < 5 && sorted(a, size, i, size-1) && partitioned(a, size, 0, i, i+1, size-1) && i >= 0 && i < size)
+ val t = sortNestedWhile(a, 0, i, size)
+ val newA = t._1
+ partitioned(newA, size, 0, i-1, i, size-1)
+ }) ensuring(_ == true)
- def sortWhile(
- j: Int, sortedArray: Map[Int,Int], i: Int, a: Map[Int,Int], i2: Int,
- size: Int, sortedArray2 : Map[Int,Int]) : (Int, Map[Int,Int], Int) =
- if ((i > 0)) {
- val t = sortNestedWhile(sortedArray, 0, sortedArray, i, size, i2, sortedArray2, a)
- sortWhile(t._2, t._1, i - 1, a, i2, size, sortedArray2)
- } else (j, sortedArray, i)
-
-
- def sortNestedWhile(
- sortedArray: Map[Int,Int], j: Int, sortedArray2 : Map[Int,Int], i: Int,
- size: Int, i2: Int, sortedArray3: Map[Int,Int], a: Map[Int,Int]) : (Map[Int,Int], Int) =
- if(j < i) {
- val newSortedArray =
- if(sortedArray(j) > sortedArray(j + 1))
- sortedArray.updated(j, sortedArray(j + 1)).updated(j+1, sortedArray(j))
- else
- sortedArray
- sortNestedWhile(newSortedArray, (j + 1), sortedArray2, i, size, i2, sortedArray3, a)
- } else (sortedArray, j)
// --------------------- sorted --------------------
-
def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
- val t = sortedWhile(true, l, l, u, a, size, l)
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
t._1
}
- def sortedWhile(
- isSorted: Boolean, k: Int, l: Int, u: Int,
- a: Map[Int,Int], size: Int, k2 : Int) : (Boolean, Int) =
- if ((k <= u)) {
- sortedWhile(
- if (a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size, k2)
- } else (isSorted, k)
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
- // ------------- partitioned ------------------
+ // ------------- partitioned ------------------
def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
- val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, l2, u1, l1, a)
- t._2
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
}
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
- def partitionedWhile(
- j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int,
- l2: Int, j2: Int, u1: Int, i2 : Int, a: Map[Int,Int]) : (Int, Boolean, Int) =
- if((i <= u1)) {
- val t = partitionedNestedWhile(
- isPartitionned, l2, l1, u1, size, j2, u2, a, l2, l2, i2, i
- )
- partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, j2, u1, i2, a)
- } else (j, isPartitionned, i)
-
- def partitionedNestedWhile(
- isPartitionned: Boolean, j: Int, l1: Int, u1: Int, size: Int, j2: Int, u2: Int,
- a: Map[Int,Int], j3 : Int, l2: Int, i2: Int, i: Int) : (Boolean, Int) =
- if (j <= u2) {
- partitionedNestedWhile(
- (if ((a(i) > a(j)))
- false
- else
- isPartitionned),
- j + 1, l1, u1, size, j2, u2, a, j3, l2, i2, i)
- } else (isPartitionned, j)
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
- //------------ isArray -------------------
+ //------------ isArray -------------------
def isArray(a: Map[Int,Int], size: Int): Boolean =
- if((size <= 0))
+ if(size <= 0)
false
else
isArrayRec(0, size, a)
@@ -86,11 +131,23 @@ object BubbleFun {
if (i >= size)
true
else {
- if (a.isDefinedAt(i))
+ if(a.isDefinedAt(i))
isArrayRec(i + 1, size, a)
else
false
}
+ // ----------------- content ------------------
+ def content(a: Map[Int, Int], size: Int): Set[Int] = {
+ require(isArray(a, size) && size < 5)
+ var i = 0
+ var s = Set.empty[Int]
+ while(i < size) {
+ s = s ++ Set(a(i))
+ i = i + 1
+ }
+ s
+ }
+
}
diff --git a/mytest/BubbleWeakInvariant.scala b/mytest/BubbleWeakInvariant.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d335cb81ffce8831f0dc1c203ab47c227d761e7f
--- /dev/null
+++ b/mytest/BubbleWeakInvariant.scala
@@ -0,0 +1,132 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object Bubble {
+
+ def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size < 5 && isArray(a, size))
+ var i = size - 1
+ var j = 0
+ var sortedArray = a
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sortedArray(j) > sortedArray(j+1)) {
+ val tmp = sortedArray(j)
+ sortedArray = sortedArray.updated(j, sortedArray(j+1))
+ sortedArray = sortedArray.updated(j+1, tmp)
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ //partitioned(sortedArray, size, 0, j-1, j, j) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < size &&
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ sorted(sortedArray, size, i, size-1)
+ )
+ sortedArray
+ }) ensuring(res => sorted(res, size, 0, size-1))
+
+ def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+ /*
+ // --------------------- sorted --------------------
+ def sorted(a: Map[Int,Int], size: Int, l: Int, u: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size)
+ val t = sortedWhile(true, l, l, u, a, size)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Map[Int,Int], size: Int) : (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l >= 0 && l <= u && u < size && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a, size)
+ } else (isSorted, k)
+ }
+ */
+
+ /*
+ // ------------- partitioned ------------------
+ def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
+ t._2
+ }
+ }
+ def partitionedWhile(j: Int, isPartitionned: Boolean, i: Int, l1: Int, size: Int, u2: Int, l2: Int, u1: Int, a: Map[Int,Int]) : (Int, Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && i >= l1)
+
+ if(i <= u1) {
+ val t = partitionedNestedWhile(isPartitionned, l2, i, l1, u1, size, u2, a, l2)
+ partitionedWhile(t._2, t._1, i + 1, l1, size, u2, l2, u1, a)
+ } else (j, isPartitionned, i)
+ }
+ def partitionedNestedWhile(isPartitionned: Boolean, j: Int, i: Int, l1: Int, u1: Int, size: Int, u2: Int, a: Map[Int,Int], l2: Int): (Boolean, Int) = {
+ require(isArray(a, size) && size < 5 && l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && j >= l2 && i >= l1 && i <= u1)
+
+ if (j <= u2) {
+ partitionedNestedWhile(
+ (if (a(i) > a(j))
+ false
+ else
+ isPartitionned),
+ j + 1, i, l1, u1, size, u2, a, l2)
+ } else (isPartitionned, j)
+ }
+ */
+
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size && isArray(a, size) && size < 5)
+ 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
+ }
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+ def rec(i: Int): Boolean = if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ if(size <= 0)
+ false
+ else
+ rec(0)
+ }
+
+}
diff --git a/mytest/LinearSearch.scala b/mytest/LinearSearch.scala
index 35e7cb300b894c954b986f26087fb14c24dd7f90..e91a3f2679b33b8b35e7d64989db1b7ade451d14 100644
--- a/mytest/LinearSearch.scala
+++ b/mytest/LinearSearch.scala
@@ -1,5 +1,7 @@
import leon.Utils._
+/* The calculus of Computation textbook */
+
object LinearSearch {
def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
diff --git a/mytest/MaxSum.scala b/mytest/MaxSum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..07c5d12ab2450cc95af964c7078759a13fe8f0cb
--- /dev/null
+++ b/mytest/MaxSum.scala
@@ -0,0 +1,70 @@
+import leon.Utils._
+
+/* VSTTE 2010 challenge 1 */
+
+object MaxSum {
+
+
+ def maxSum(a: Map[Int, Int], size: Int): (Int, Int) = ({
+ require(isArray(a, size) && size < 5 && isPositive(a, size))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < size) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && /*isGreaterEq(a, i, max) &&*/ /*(if(i == 0) max == 0 else true) &&*/ i >= 0 && i <= size)
+ (sum, max)
+ }) ensuring(res => res._1 <= size * res._2)
+
+/*
+ def isGreaterEq(a: Map[Int, Int], size: Int, n: Int): Boolean = {
+ require(size <= 5 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) > n)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+ */
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(size <= 5 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+}
diff --git a/mytest/Mult.scala b/mytest/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..417e9e9cdc74440ccac679b2d55bac33a6381e4a
--- /dev/null
+++ b/mytest/Mult.scala
@@ -0,0 +1,26 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+object Mult {
+
+ def mult(x : Int, y : Int): Int = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) invariant(r == x * (y - n) && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) invariant(r == x * (y - n) && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+}
+
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 5de2c671af169d9bd9671a7f4c340cbd6548df3e..6458079be4ef662a49bd25ea2f118f8df73ce56f 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -7,13 +7,9 @@ import purescala.TypeTrees._
import Extensions._
import scala.collection.mutable.{Set => MutableSet}
-class Analysis(pgm : Program, val reporter: Reporter = Settings.reporter) {
+class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) {
Extensions.loadAll(reporter)
- println("Analysis on program:\n" + pgm)
- val passManager = new PassManager(Seq(EpsilonElimination, ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
- val program = passManager.run(pgm)
-
val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
@@ -75,6 +71,11 @@ class Analysis(pgm : Program, val reporter: Reporter = Settings.reporter) {
allVCs ++= tactic.generatePostconditions(funDef).sortWith(vcSort)
allVCs ++= tactic.generateMiscCorrectnessConditions(funDef).sortWith(vcSort)
}
+ allVCs = allVCs.sortWith((vc1, vc2) => {
+ val id1 = vc1.funDef.id.name
+ val id2 = vc2.funDef.id.name
+ if(id1 != id2) id1 < id2 else vc1 < vc2
+ })
}
val notFound: Set[String] = Settings.functionsToAnalyse -- analysedFunctions
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index 6f31b9ff59bc4b4681e7284c4dc3479400585534..a01d025431c2ec3c704a1950410334fd322abae9 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -78,7 +78,10 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
expr2
}
}
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ if(functionDefinition.fromLoop)
+ Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
+ else
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
}
}
@@ -107,11 +110,18 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
val newBody : Expr = replace(substMap, prec)
val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
- new VerificationCondition(
- withPrecIfDefined(path, newCall),
- function,
- VCKind.Precondition,
- this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
+ if(fd.fromLoop)
+ new VerificationCondition(
+ withPrecIfDefined(path, newCall),
+ fd.parent.get,
+ if(fd == function) VCKind.InvariantInd else VCKind.InvariantInit,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(fd)
+ else
+ new VerificationCondition(
+ withPrecIfDefined(path, newCall),
+ function,
+ VCKind.Precondition,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
}).toSeq
} else {
Seq.empty
@@ -141,7 +151,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- function,
+ if(function.fromLoop) function.parent.get else function,
VCKind.ExhaustiveMatch,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
@@ -173,7 +183,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- function,
+ if(function.fromLoop) function.parent.get else function,
VCKind.MapAccess,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 75f827cb243059ad6eb19b44d7bb235a8c45d58d..7214b0d826658b4f9c03d8afb703ca50d739b3cc 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -981,6 +981,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case errorType => scala.sys.error("Unexpected type for singleton map: " + (ex, errorType))
}
case e @ EmptyMap(fromType, toType) => {
+ typeToSort(e.getType) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
val fromSort = typeToSort(fromType)
val toSort = typeToSort(toType)
z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
@@ -1229,7 +1230,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
val startingVar : Identifier = FreshIdentifier("start", true).setType(BooleanType)
val result = treatFunctionInvocationSet(startingVar, true, functionCallsOf(formula))
- reporter.info(result)
+ //reporter.info(result)
(Variable(startingVar) +: formula +: result._1, result._2)
}
}
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index ba1c793d376439450cb4565b764014f7c73aa4ae..4d76cd8b5e714b9799cc90b9ca0b6802de116ceb 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -51,6 +51,8 @@ object FunctionClosure extends Pass {
val newVarDecls = varDecl ++ extraVarDecls
val newFunId = FreshIdentifier(id.name)
val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
+ newFunDef.fromLoop = fd.fromLoop
+ newFunDef.parent = fd.parent
val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
@@ -61,7 +63,7 @@ object FunctionClosure extends Pass {
newFunDef.postcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
- case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)))
+ case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)).setPosInfo(fi))
case _ => None
}
val freshBody = fd.body.map(b => replace(freshVarsExpr, b))
@@ -73,17 +75,13 @@ object FunctionClosure extends Pass {
newFunDef.body = recBody2
def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
- case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)))
+ case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
case _ => None
}
val recRest = functionClosure(rest, bindedVars)
val recRest2 = searchAndReplaceDFS(substFunInvocInRest)(recRest)
LetDef(newFunDef, recRest2).setType(l.getType)
}
-
- //case fi @ FunctionInvocation(fd, args) => {
-
- //}
case l @ Let(i,e,b) => {
val re = functionClosure(e, bindedVars)
pathConstraints ::= Equals(Variable(i), re)
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
index 799cea51aa28945996b6307d27de4fde7eec1867..2e92ef23568783deb28971ea9d1a5c0bdbe2e34e 100644
--- a/src/main/scala/leon/FunctionHoisting.scala
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -70,7 +70,7 @@ object FunctionHoisting extends Pass {
(GuardedCase(pat, guard, r), s)
}
}.unzip
- (MatchExpr(scrutRes, csesRes).setType(m.getType), csesSets.toSet.flatten ++ scrutSet)
+ (MatchExpr(scrutRes, csesRes).setType(m.getType).setPosInfo(m), csesSets.toSet.flatten ++ scrutSet)
}
case t if t.isInstanceOf[Terminal] => (t, Set())
case unhandled => scala.sys.error("Non-terminal case should be handled in searchAndReplace: " + unhandled)
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index cb14cc02a9b4d116a2fd17774c3f2e6dadd65135..662ed9cc9e8ce207b004ecba81f83af41ea1446c 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -10,10 +10,12 @@ object ImperativeCodeElimination extends Pass {
val description = "Transform imperative constructs into purely functional code"
private var varInScope = Set[Identifier]()
+ private var parent: FunDef = null //the enclosing fundef
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
+ parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
}))
@@ -107,7 +109,7 @@ object ImperativeCodeElimination extends Pass {
val matchExpr = MatchExpr(scrutRes, cses.zip(newRhs).map{
case (SimpleCase(pat, _), newRhs) => SimpleCase(pat, newRhs)
case (GuardedCase(pat, guard, _), newRhs) => GuardedCase(pat, replaceNames(scrutFun, guard), newRhs)
- }).setType(matchType)
+ }).setType(matchType).setPosInfo(m)
val scope = ((body: Expr) => {
val tupleId = FreshIdentifier("t").setType(matchType)
@@ -140,10 +142,12 @@ object ImperativeCodeElimination extends Pass {
val whileFunVarDecls = whileFunVars.map(id => VarDecl(id, id.getType))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
val whileFunDef = new FunDef(FreshIdentifier("while"), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
+ whileFunDef.fromLoop = true
+ whileFunDef.parent = Some(parent)
val whileFunCond = condRes
val whileFunRecursiveCall = replaceNames(condFun,
- bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable))))
+ bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable)).setPosInfo(wh)))
val whileFunBaseCase =
(if(whileFunVars.size == 1)
condFun.get(modifiedVars.head).getOrElse(whileFunVars.head).toVariable
@@ -182,7 +186,7 @@ object ImperativeCodeElimination extends Pass {
LetDef(
whileFunDef,
Let(tupleId,
- FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)),
+ FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)).setPosInfo(wh),
if(finalVars.size == 1)
Let(finalVars.head, tupleId.toVariable, body)
else
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index aefcf528a0c83593f806374bdc21688c5d2a15bc..72623c96a2c732b4dac1995392545474c7f3f9c7 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,7 +31,9 @@ object Main {
}
private def defaultAction(program: Program, reporter: Reporter) : Unit = {
- val analysis = new Analysis(program, reporter)
+ val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
+ val program2 = passManager.run(program)
+ val analysis = new Analysis(program2, reporter)
analysis.analyse
}
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
index 5381b7bee6a389ac120477c8316fcf1e97ccdc62..f2830df79bfa129ce93d58157110a2107453595a 100644
--- a/src/main/scala/leon/PassManager.scala
+++ b/src/main/scala/leon/PassManager.scala
@@ -6,9 +6,9 @@ class PassManager(passes: Seq[Pass]) {
def run(program: Program): Program = {
passes.foldLeft(program)((pgm, pass) => {
- println("Running Pass: " + pass.description)
+ //println("Running Pass: " + pass.description)
val newPgm = pass(pgm)
- println("Resulting program: " + newPgm)
+ //println("Resulting program: " + newPgm)
newPgm
})
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 2818d6b2a89e5de863d4d8839f6b092d3ab261fd..9e7055638b46d401a55d9a49866ad8bc0e7751e3 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -24,4 +24,5 @@ object Settings {
var useParallel : Boolean = false
// When this is None, use real integers
var bitvectorBitwidth : Option[Int] = None
+ var verbose : Boolean = false
}
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index d7c9781386cd9630d0f2372900678c318c2e7155..2f5f1bc53fc000242758f19aee766cf175dadf84 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -20,6 +20,8 @@ object UnitElimination extends Pass {
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.args.exists(vd => vd.tpe == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+ freshFunDef.fromLoop = fd.fromLoop
+ freshFunDef.parent = fd.parent
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
fun2FreshFun += (fd -> freshFunDef)
@@ -135,7 +137,7 @@ object UnitElimination extends Pass {
case GuardedCase(pat, guard, rhs) => GuardedCase(pat, removeUnit(guard), removeUnit(rhs))
}
val tpe = csesRec.head.rhs.getType
- MatchExpr(scrutRec, csesRec).setType(tpe)
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
}
case _ => sys.error("not supported: " + expr)
}
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 4150536fa441352761a7542019caa64d478b0d6a..01545bc3e87bd3606591b464f59098a5b0d8dd8c 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -49,4 +49,7 @@ object VCKind extends Enumeration {
val Postcondition = Value("postcond.")
val ExhaustiveMatch = Value("match.")
val MapAccess = Value("map acc.")
+ val InvariantInit = Value("inv init.")
+ val InvariantInd = Value("inv ind.")
+ val InvariantPost = Value("inv post.")
}
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index c08d745721bf331a029129459c4daab0299fa22b..c6757f2cb87a6e2ee0d12403b788a3589ef8da71 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -727,13 +727,13 @@ trait CodeExtraction extends Extractors {
val rr = rec(t2)
MultisetPlus(rl, rr).setType(rl.getType)
}
- case ExApply(lhs,args) => {
+ case app@ExApply(lhs,args) => {
val rlhs = rec(lhs)
val rargs = args map rec
rlhs.getType match {
case MapType(_,tt) =>
assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt)
+ MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
case FunctionType(fts, tt) => {
rlhs match {
case Variable(id) =>
@@ -757,8 +757,6 @@ trait CodeExtraction extends Extractors {
IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
}
case lc @ ExLocalCall(sy,nm,ar) => {
- println("Got local call with: " + sy + ": " + nm)
- println(defsToDefs)
if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
if(!silent)
unit.error(tr.pos, "Invoking an invalid function.")
@@ -812,7 +810,10 @@ trait CodeExtraction extends Extractors {
if(handleRest) {
rest match {
- case Some(rst) => PBlock(Seq(psExpr), rec(rst))
+ case Some(rst) => {
+ val recRst = rec(rst)
+ PBlock(Seq(psExpr), recRst).setType(recRst.getType)
+ }
case None => psExpr
}
} else {
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index f22b044b92541ee75c5f00e5500bfbccf7a3bf60..0db7fa99c7694b0f3fe4e1d2295f4726e0aa09cb 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -40,7 +40,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
" --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
- " --noverifymodel Do not verify the correctness of models returned by Z3"
+ " --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
+ " --verbose Print debugging informations"
)
/** Processes the command-line options. */
@@ -63,7 +64,11 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
case "noLuckyTests" => leon.Settings.luckyTest = false
+<<<<<<< HEAD
case "noverifymodel" => leon.Settings.verifyModel = false
+=======
+ case "verbose" => leon.Settings.verbose = true
+>>>>>>> leon2
case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index efd8b52fb31e7cd4d61ff868bba3c836ca1f0e2e..f2da8a7cef1f1f3b0290a35a260f40ceefbf6705 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -283,6 +283,11 @@ object Definitions {
var precondition: Option[Expr] = None
var postcondition: Option[Expr] = None
+ //true if this function has been generated from a while loop
+ var fromLoop = false
+ //the fundef where the loop was defined (if applies)
+ var parent: Option[FunDef] = None
+
def hasImplementation : Boolean = body.isDefined
def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index cb0ce8a1867232d277df2892ca522a9fd1ed8645..6155d5da99d76f66a97dc6425690dcc26b8f8f02 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -18,9 +18,9 @@ object Trees {
}
case class Block(exprs: Seq[Expr], last: Expr) extends Expr {
- val t = last.getType
- if(t != Untyped)
- setType(t)
+ //val t = last.getType
+ //if(t != Untyped)
+ // setType(t)
}
case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType {
@@ -369,7 +369,7 @@ object Trees {
case class SingletonMap(from: Expr, to: Expr) extends Expr
case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr
- case class MapGet(map: Expr, key: Expr) extends Expr
+ case class MapGet(map: Expr, key: Expr) extends Expr with ScalacPositional
case class MapUnion(map1: Expr, map2: Expr) extends Expr
case class MapDifference(map: Expr, keys: Expr) extends Expr
case class MapIsDefinedAt(map: Expr, key: Expr) extends Expr with FixedType {
@@ -439,7 +439,7 @@ object Trees {
case MultisetPlus(t1,t2) => Some((t1,t2,MultisetPlus))
case MultisetDifference(t1,t2) => Some((t1,t2,MultisetDifference))
case SingletonMap(t1,t2) => Some((t1,t2,SingletonMap))
- case MapGet(t1,t2) => Some((t1,t2,MapGet))
+ case mg@MapGet(t1,t2) => Some((t1,t2, (t1, t2) => MapGet(t1, t2).setPosInfo(mg)))
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
@@ -1284,7 +1284,7 @@ object Trees {
def rewriteMapGet(e: Expr) : Option[Expr] = e match {
case mg @ MapGet(m,k) =>
val ida = MapIsDefinedAt(m, k)
- Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType)).setType(mg.getType))
+ Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType).setPosInfo(mg)).setType(mg.getType))
case _ => None
}