mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

fix part of #5519

Browse source 
generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right.
This commit is contained in:
Nikolaj Bjorner 2021-08-31 20:06:06 -07:00
parent 7c782a7ef8
commit 90f98d5791
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_seq.cpp
View file

@ -187,14 +187,18 @@ extern "C" {
svector<char> buff; svector<char> buff;
for (unsigned i = 0; i < str.length(); ++i) { for (unsigned i = 0; i < str.length(); ++i) {
unsigned ch = str[i]; unsigned ch = str[i];
if (ch >= 256) { if (ch <= 32 || ch >= 127) {
buff.reset(); buff.reset();
buffer.push_back('\\'); buffer.push_back('\\');
buffer.push_back('\\'); // possibly replace by native non-escaped version? buffer.push_back('\\'); // possibly replace by native non-escaped version?
buffer.push_back('u'); buffer.push_back('u');
buffer.push_back('{'); buffer.push_back('{');
while (ch > 0) { while (ch > 0) {
buff.push_back('0' + (ch & 0xF)); unsigned d = ch & 0xF;
if (d < 10)
buff.push_back('0' + d);
else
buff.push_back('a' + (d - 10));
ch /= 16; ch /= 16;
} }
for (unsigned j = buff.size(); j-- > 0; ) { for (unsigned j = buff.size(); j-- > 0; ) {