leon
leon copied to clipboard
Bug in ImperativeCodeElimination
The following program makes Leon's ImperativeCodeElimination crash.
object Dummy {
case class M(var value: Int)
def barM(m: M) = {
m.value = m.value + 1
303
}
def foo(m: M) = m match {
case n: M => barM(n)
}
}
Stacktrace looks like:
java.lang.AssertionError: assertion failed
at scala.Predef$.assert(Predef.scala:156)
at leon.xlang.ImperativeCodeElimination$.leon$xlang$ImperativeCodeElimination$$toFunction(ImperativeCodeElimination.scala:75)
at leon.xlang.ImperativeCodeElimination$$anonfun$20.apply(ImperativeCodeElimination.scala:177)
at leon.xlang.ImperativeCodeElimination$$anonfun$20.apply(ImperativeCodeElimination.scala:175)
at scala.collection.immutable.List$$anonfun$foldRight$1.apply(List.scala:397)
at scala.collection.LinearSeqOptimized$class.foldLeft(LinearSeqOptimized.scala:124)
at scala.collection.immutable.List.foldLeft(List.scala:84)
at scala.collection.immutable.List.foldRight(List.scala:397)
at leon.xlang.ImperativeCodeElimination$.leon$xlang$ImperativeCodeElimination$$toFunction(ImperativeCodeElimination.scala:175)
at leon.xlang.ImperativeCodeElimination$.leon$xlang$ImperativeCodeElimination$$toFunction(ImperativeCodeElimination.scala:200)
at leon.xlang.ImperativeCodeElimination$$anonfun$44.apply(ImperativeCodeElimination.scala:376)
at leon.xlang.ImperativeCodeElimination$$anonfun$44.apply(ImperativeCodeElimination.scala:374)
When this is fixed, src/test/resources/regression/genc/unverified/Inheritance9.scala
should be moved to src/test/resources/regression/genc/valid/Inheritance9.scala
.