cbmc --verbosity 10 --xml-ui invariant failure

[markrtuttle]

CBMC version: 5.61.0
Operating system: MacOS 11.6.7

Create the file main.c

#include<assert.h>

int main() {
  int x;
  assert(x);
}

and run the command

cbmc --verbosity 10 --xml-ui main.c

and cbmc fails with

--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20220707-65576-1rz4dy2/src/util/xml.cpp:113 function: escape
Condition: ch >= ' '
Reason: XML does not support escaping non-printable character 226
Backtrace:
...
--- end invariant violation report ---
Abort trap: 6

I think the problem is that --verbosity 10 generates lines like

ASSERT ¬(main::1::x!0@1#1 = 0)

and the character ¬ is extended ASCII character 170 (I can't explain the 226 in the error message). In xml.cpp, line 113 asserts the data invariant ch > ' ' but since ch=170 interpreted as a signed character is negative, the assertion fails and the invariant failure is thrown. I think the check ch > ' ' is intended to skip the unprintable characters below the space character in ASCII, but I think the extended ASCII characters above 128 are mostly printable characters and should be okay.

[jimgrundy]

This is a real pain that has bitten a few of us recently. It's really hard to debug for the user as it gives you no hint as to where and in what file you need to find the offending character.

[thomasspriggs]

The 128-255 range does potentially open up a can of character encoding worms. But they certainly correspond to printable characters for (code page dependant) extended ascii or part of a multi-byte sequence for many printable UTF-8 characters. In this case I think it is the ⇔ character which is encoded as 0xE2 0x87 0x94 or 226 135 148 in decimal. This is from the line __CPROVER_malloc_is_new_array#1 ⇔ false in the output.

I agree with Mark's assessment. The check should probably be (unsigned char)ch >= 32. @tautschnig Any comment from you on this, given that git-blame says you added this condition?

[thomasspriggs]

PR #7109 which should address this issue has now been merged. @markrtuttle Can you confirm whether you are satisfied with the current solution so we can close out this issue?

[tautschnig]

I agree with Mark's assessment. The check should probably be (unsigned char)ch >= 32. @tautschnig Any comment from you on this, given that git-blame says you added this condition?

Thanks you @thomasspriggs for fixing the bug that I had introduced! I had just failed to take into account signedness.