leon icon indicating copy to clipboard operation
leon copied to clipboard

Bug in ImperativeCodeElimination

Open mantognini opened this issue 7 years ago • 0 comments

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.

mantognini avatar Dec 15 '16 10:12 mantognini