-
Notifications
You must be signed in to change notification settings - Fork 254
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Dafny string literals with surrogate characters compiled to invalid Go strings #1980
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: golang
Dafny's transpiler to Go and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Comments
See also #413 |
Note that this really depends on the proper, deeper fix proposed in dafny-lang/rfcs#13, because another case is a string with invalid uses of surrogate characters that cannot be losslessly expressed as a Go string. |
This was referenced Oct 25, 2022
robin-aws
added a commit
that referenced
this issue
Nov 3, 2022
…and Go (#2926) Fixes #1980. Fixes #2925. Should fix the root cause of #2934, but I'm not claiming the complete fix, as attempting to include unescaped, non-ASCII characters in a Dafny source file is revealing platform-specific headaches in the integration test runner I'd like to address in a separate PR. Printing non-ASCII characters, especially invalid UTF-16 sequences, is still inconsistent across backends, but at least should not crash after this change. Again this is difficult to test effectively across platforms in our testing architecture. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> Co-authored-by: Clément Pit-Claudel <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: golang
Dafny's transpiler to Go and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Dafny string literals are translated literally to Go literals, but
\uXXXX
in Dafny is interpreted as a UTF-16 code point, whereas Go will interpret the same escape sequences as Unicode scalar values, which excludes surrogates.The text was updated successfully, but these errors were encountered: