Bug in RecursionCountInstrumenter(?)

[mantognini]

The following program make verification crash, apparently in RecursionCountInstrumenter, but the bug might be due to some other component.

/* Copyright 2009-2016 EPFL, Lausanne */

import leon.annotation.extern

object Aliasing3 {

  case class MutableInteger(var x: Int)

  def scope = {
    var x = 0

    def hoo(m: MutableInteger) {
      toto()
      foo(42, m)
    }

    def foo(y: Int, m: MutableInteger) {
      toto()
      x = 1
      bar(m)
      m.x = y
    }

    foo(42, MutableInteger(58))

    val m = MutableInteger(58)

    hoo(m)

    def goo(y: Int) {
      foo(y, m)
    }
    goo(42)

    m.x
  } ensuring { _ == 42 }

  def bar(m: MutableInteger) {
    m.x = 0
  }

  def toto() = { }

  def _main(): Int = {
    if (scope == 42) 0
    else 1
  } ensuring { _ == 0 }

  @extern
  def main(args: Array[String]): Unit = _main()
}

Stacktrace looks like this:

java.util.NoSuchElementException: key not found: def foo$1(y$6 : Int, m$5 : MutableInteger$0): (Unit, MutableInteger$0) = {
  var m$8 = m$5
  ({
    toto$0
    x$25 = 1
    val res$203 = bar$1(m$8)
    m$8 = res$203._2
    res$203._1
    m$8 = MutableInteger$0(y$6)
  }, m$8)
}
    at scala.collection.MapLike$class.default(MapLike.scala:228)
    at scala.collection.AbstractMap.default(Map.scala:59)
    at scala.collection.mutable.HashMap.apply(HashMap.scala:65)
    at leon.invariant.datastructure.DirectedGraph.successors(Graph.scala:178)
    at leon.invariant.datastructure.Graph$class.search$1(Graph.scala:109)
    at leon.invariant.datastructure.Graph$class.processNeighbor$1(Graph.scala:99)
    at leon.invariant.datastructure.Graph$$anonfun$1.apply(Graph.scala:109)
    at leon.invariant.datastructure.Graph$$anonfun$1.apply(Graph.scala:109)
    at scala.collection.TraversableOnce$$anonfun$foldLeft$1.apply(TraversableOnce.scala:157)
    at scala.collection.TraversableOnce$$anonfun$foldLeft$1.apply(TraversableOnce.scala:157)
    at scala.collection.immutable.Set$Set1.foreach(Set.scala:94)
    at scala.collection.TraversableOnce$class.foldLeft(TraversableOnce.scala:157)
    at scala.collection.AbstractTraversable.foldLeft(Traversable.scala:104)
    at leon.invariant.datastructure.Graph$class.search$1(Graph.scala:109)
    at leon.invariant.datastructure.Graph$$anonfun$sccs$2.apply(Graph.scala:130)
    at leon.invariant.datastructure.Graph$$anonfun$sccs$2.apply(Graph.scala:129)
    at scala.Option.foreach(Option.scala:257)
    at leon.invariant.datastructure.Graph$class.sccs(Graph.scala:129)
    at leon.invariant.datastructure.DirectedGraph.sccs(Graph.scala:143)
    at leon.transformations.RecursionCountInstrumenter.<init>(RecursionCountInstrumenter.scala:19)
    at leon.transformations.InstrumentationPhase$$anonfun$1.apply(SerialInstrumentationPhase.scala:37)

When this is fixed, src/test/resources/regression/genc/unverified/Aliasing3.scala should be moved to src/test/resources/regression/genc/valid/Aliasing3.scala (ATM only available on topic/genc_v2 branch).