String support?

[mwookawa]

It seems string operations are unsupported

object asdf { def testString(s: String):Boolean = s.isEmpty }

Stainless error: stainless.frontend.package$UnsupportedCodeException: Unknown call to isEmpty on s (String) with arguments List() of type List()

We have a number of methods manipulating strings that we can't just ignore. Is there a workaround?

[jad-hamza]

For isEmpty it should be easy to change CodeExtraction.scala to support it. What are the other methods that you need? Maybe they can also be encoded using Stainless trees on strings.

On the user side, I'm not sure much can be done, except replacing String by a user-defined type with user-defined functions.

[mwookawa]

This also applies to StringBuffer, and I think StringBuilder; length, isEmpty, charAt, append are the most commonly used.

apply actually does work, so i've used that to write some hand implementations to make the verifier happy for now, but it would be awesome if we could get this support natively

[vkuncak]

Also, this fails with a rather obscure stack trace. We should either support a bit more or handle better uknown dependencies:

import stainless.collection._
import stainless.lang._

object test_input_strings {
  def test: Char = {
    val s: String = "abc"
    s(0)
  }
}