nedbrek / Atlantis

Main Atlantis development Repository
GNU General Public License v2.0
10 stars 3 forks source link

json report backslash escapes #192

Open sheckman16 opened 1 year ago

sheckman16 commented 1 year ago

It would be convenient if unit names containing backslashes (like "##/") escaped the backslashes in json. I wish for "name": "\\##/ (2918)" instead of the present encoding, which is "name": "\##/ (2918)"

I wish for this because the default python json decoder chokes on the existing report.

Mochnant commented 1 year ago

That's actually a forward slash, not a backslash, which isn't required to be escaped in the json specification, but it is permitted to be if useful.

sheckman16 commented 1 year ago

I suspect github formatting is making the four character name you see different than the four characters I typed. Let me try again, without trying to enter any "reverse solidus" characters in my comment.

The troublesome name consists of the four characters, ascii 92, ascii 35, ascii 35, ascii 47. In order, I would name these "backslash", "octothorpe", "octothorpe", "forward slash". RFC 8259 names ascii 92 "reverse solidus", and ascii 47 "solidus".

RFC 8259 reads:

All Unicode characters may be placed within the quotation marks, except for the characters that MUST be escaped: quotation mark, reverse solidus, and the control characters (U+0000 through U+001F).

The problem with the four character name of unit 2918 is the first character, ascii 92. Python's json decoder, following RFC 8259, thinks ascii 92 (the reverse solidus) must be escaped, so interprets ascii 92 followed by ascii 35 in the JSON as the undefined escape sequence "(reverse solidus)(octothorpe)".