It's not a bug though. It's part of the current formal semantics of strings
in K. K does not have the \b escape. If you want to represent the string
"a\bc" in K, you should write "a\x08c". They correspond to the same exact
sequence of unicode code points, they just obey different conventions for
expressing and escaping strings.

If you want the \b escape in your language, you should manually construct a
MyString token sort with exactly the regular expression you want. If on the
other hand you want to have "strings" be completely unprocessed in K, you
can also do that, but then things like substring and find will not work at
all how you expect them to.

The String sort is designed to represent the mathematical domain of unicode
character strings: it is not designed to represent the syntax of Strings in
any particular language other than K.


On Tue, Apr 22, 2014 at 3:41 PM, Radu Mereuta <notifications@github.com>wrote:

> In src/javasources/KTool/src/org/kframework/kil/Token.java:
>
> > @@ -50,7 +50,7 @@ public static KApp kAppOf(String sort, String value) {
> >          } else if (sort.equals(IntBuiltin.SORT_NAME)) {
> >              return IntBuiltin.kAppOf(value);
> >          } else if (sort.equals(StringBuiltin.SORT_NAME)) {
> > -            return StringBuiltin.kAppOf(value);
> > +            return StringBuiltin.kAppOf(StringUtil.unquoteString(value));
>
> Actually, I consider this to be a hack.
> I think we shouldn't unquote strings when we represent them in the memory.
> I'm saying this because Daejun had some problems in the javascript
> semantics when we didn't handle properly some special characters.
>
> For example, if you write in a program "a\bc" after it goes through
> kompile and krun, you will get the result "abc" (notice the backslash
> disappeared). Now that's a bug, we need to handle it somehow. But not in
> this commit. I just followed the convention we currently have in this case.
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/397/files#r11874724>
> .
>