AntiAliasing does not always preserve contracts structure

[mario-bucev]

All specifications remain, but the postcondition may not always be preserved at the top level.
For instance, the following snippet:

import stainless._
import stainless.lang._
import stainless.annotation._

object EnsuringTestEtAl2 {

  @pure
  def upd(arr: Array[BigInt], i: Int): (Array[BigInt], Int) = {
    require(0 <= i && i < arr.length - 10)
    (freshCopy(arr).updated(i, 1234), 1234)
  }

  def app(arr: Array[BigInt], i: Int): Unit = {
    decreases(i)
    require(0 <= i && i < arr.length - 10)
    val (arr2, x) = upd(arr, i)
    {
      if (i == 0) ()
      else {
        val (arr3, xyz) = upd(arr2, i)
        app(arr3, i - 1)
      }
    }.ensuring { _ => i < arr.length }
  }
}

causes an interesting error in the TypeChecker:

[ Fatal  ] EnsuringTestEtAl2.scala:32:9: Call to function app is not allowed here, because it is mutually recursive with the current function app
                   app(arr3, i - 1)
                   ^^^^^^^^^^^^^^^^

The tree after AntiAliasing may be an explanation:

def app$0(arr$1: Array[BigInt], (i$27: Int) @pure): Unit = {
  decreases(i$27)
  require(0 <= i$27 && i$27 < arr$1.length - 10)
  val targetBound$0: (Array[BigInt], Int) = upd$0(arr$1, i$27)
  var $1$$2: (Array[BigInt], Int) = (targetBound$0 match {
    case (arr2$1, x$100) =>
      val arr2$2: Array[BigInt] = targetBound$0._1
      (arr2$2, x$100)
  })
  val res$43: Unit = {
    val arr2$0: Array[BigInt] = $1$$2._1
    val x$99: Int = $1$$2._2
    {
      val targetBound$1: Boolean = i$27 == 0
      if (targetBound$1) {
        ()
      } else {
        val targetBound$2: (Array[BigInt], Int) = upd$0(arr2$0, i$27)
        var $2$$1: (Array[BigInt], Int) = (targetBound$2 match {
          case (arr3$1, xyz$1) =>
            val arr3$2: Array[BigInt] = targetBound$2._1
            (arr3$2, xyz$1)
        })
        val res$42: Unit = {
          val arr3$0: Array[BigInt] = $2$$1._1
          val xyz$0: Int = $2$$1._2
          app$0(arr3$0, i$27 - 1)
        }
        res$42
      }
    } ensuring { // No longer top-level!
      (_$1$11: Unit) => i$27 < arr$1.length
    }
  }
  res$43
}