Skip to content

Commit 8691d65

Browse files
committed
Allow characters with value >= 128 in XML output
These values are used as part of printable characters which should be allowed in XML output. This invariant was previously violated for characters such as `¬` and `⇔` which are included in the output when cbmc is invoked with `--verbosity 10 --xml-ui`. This was due to the comparison formerly being a signed comparison. So byte values in the range 128 to 255 were treated as values in the -128 to -1 range which are less than ` ` which has value 32.
1 parent 2181146 commit 8691d65

File tree

3 files changed

+23
-2
lines changed

3 files changed

+23
-2
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --xml-ui
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
VERIFICATION FAILED
7+
⇔ false
8+
\¬main\:\:1\:\:x\!0\@1\#1
9+
--
10+
XML does not support escaping non-printable character
11+
--
12+
Test that running cbmc with --verbosity 10 and --xml-ui does not violate any
13+
xml printing invariants.
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#include <assert.h>
2+
3+
int main(void)
4+
{
5+
__CPROVER_bool x;
6+
__CPROVER_assume(!x);
7+
assert(0);
8+
}

src/util/xml.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ void xmlt::escape(const std::string &s, std::ostream &out)
108108

109109
default:
110110
DATA_INVARIANT(
111-
ch >= ' ',
111+
static_cast<unsigned char>(ch) >= 32u,
112112
"XML does not support escaping non-printable character " +
113113
std::to_string((unsigned char)ch));
114114
out << ch;
@@ -149,7 +149,7 @@ void xmlt::escape_attribute(const std::string &s, std::ostream &out)
149149

150150
default:
151151
DATA_INVARIANT(
152-
ch >= ' ',
152+
static_cast<unsigned char>(ch) >= 32u,
153153
"XML does not support escaping non-printable character " +
154154
std::to_string((unsigned char)ch));
155155
out << ch;

0 commit comments

Comments
 (0)