search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 49 forks source link

Well-formedness check failure when operating on an `Array` type alias #1529

Closed mario-bucev closed 1 month ago

mario-bucev commented 1 month ago

The following code is rejected after extraction:

object ArrayTypeAlias {
  type ByteArray = Array[Byte]

  case class ByteArrayWrapper(ba: ByteArray)

  def test(baw: ByteArrayWrapper): Unit = {
    require(baw.ba.length == 64)
    baw.ba(0) = 3
    val ba2 = baw.ba.updated(0, 4.toByte)
    assert(ba2(0) == 4)
  }
}

Note that it seems to only concern Arrays, Set etc. are unaffected. The fix is easy but I'm opening the issue for tracking.