f180c9ce17
This PR fixes a bug in EmitC that can be caused by working with the
string literal `"\x01abc"` in
Lean and causes a C compiler error.
The error is as follows:
```
run.c:29:189: error: hex escape sequence out of range
29 | static const lean_string_object l_badString___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 5, .m_capacity = 5, .m_length = 4, .m_data = "\x01abc"};
| ^~~~~~~
1 error generated.
```
This happens as hex escape sequences can be arbitrarily long while lean
expects them to cut off
after two chars. Thus, the C compiler parses the string as one large hex
escape sequence `01abc` and
subsequently notices this is too large.
Discovered by @datokrat
12 lines
332 B
Text
12 lines
332 B
Text
module
|
|
|
|
def badString : String := "\x01abc"
|
|
|
|
public def main : IO Unit := do
|
|
IO.println s!"length = {badString.length}"
|
|
IO.println s!"utf8Size = {badString.utf8ByteSize}"
|
|
let ba := badString.toUTF8
|
|
IO.println s!"toUTF8.size = {ba.size}"
|
|
IO.print "bytes:"
|
|
for i in 0...ba.size do IO.print s!" {ba[i]!}"
|
|
IO.println ""
|