kframework/k — pull request #299 by radumereuta (2014-03-22 03:50:36+00:00)
Title: Fixing StringUtil escape not taking into consideration '\f'.

Daejun found this problem when you would write in a string "\f" and the result after processing through K would be "f".
The problem was with the way we esacpe and unescape strings internally. When we load a StringBuiltin, we try to use the internal representation, meaning "\n" would be transformed into the string that contains the new line character.

The way unescape works right now, makes it that "\a" would be converted into "a". Completely removing the backslash character. At one point we had a request from Denis I believe to allow almost everything to be escaped, and the definition would take care of escaping those into something that the backend would understand.

In this patch I've fixed the case of '\f', but there are still the other cases. I think the backend should reject (throw an exception) if it doesn't know how to unescape something.