leon icon indicating copy to clipboard operation
leon copied to clipboard

Evaluation of passes fails to record positions of patterns, guards, scrutinees

Open colder opened this issue 8 years ago • 1 comments

The counter-example is not well displayed within the passes:

package leon.custom

import leon._
import leon.lang._
import leon.collection._
import leon.annotation._

sealed abstract class List[T] {  
  def count(e: T): BigInt = { this match {
    case Cons(h, t) =>
      if (h == e) {
        t.count(e)
      } else {
        t.count(e)
      }
    case Nil() =>
      BigInt(0)
  }} ensuring { res => 
    (((this, e), res) passes {
      case (Cons(a1, Cons(a2, Cons(a3, Cons(a4, Nil())))), v) if a1 == v && a2 == v && a3 != v && a4 == v => 3
      case (Cons(a1, Cons(a2, Nil())), v) if a1 != v && a2 != v => 0
    })
  }

}


case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]

colder avatar Dec 08 '15 15:12 colder

What is it supposed to display ? Or where ?

MikaelMayer avatar Jan 07 '16 13:01 MikaelMayer