Invalid UTF

[sorawee]

From https://mnaoumov.wordpress.com/2014/06/14/stripping-invalid-characters-from-utf-16-strings/:

"\ud800b" is invalid because "here \ud800 is lead surrogate but it is followed by b letter which is not a low surrogate."

But

method Main() {
  print "\ud800b";
}

works fine, and outputs �b

Ideally, this should result in a verification error.

Reported by @jswrenn

[cpitclaudel]

Dafny strings are not valid unicode strings, currently, so I would say "not a bug"; we are in the process of revamping those strings in dafny-lang/rfcs#13

[robin-aws]

Hi Sorawee! The new --unicode-char option, which will be on by default in Dafny 4.0, mostly addresses this gap. When it is enabled, the \uXXXX style of unicode escapes that identifies UTF-16 code points is no longer accepted, in favor of the \U{X...X} style that identifies Unicode scalar values instead. That means it's no longer possible to specify invalid strings like the one in the example. See https://dafny.org/latest/DafnyRef/DafnyRef#sec-characters for further details.

Even better, Dafny supports arbitrary Unicode characters directly in string literals now, so you no longer have to use Unicode escapes for such characters.

Closing this as I believe we've done everything we're planning to do in this area, but feel free to reopen!