mirror of
https://github.com/Z3Prover/z3
synced 2026-05-25 03:16:21 +00:00
Fix DEL character encoding in string literals
Change condition from `ch >= 128` to `ch >= 127` to include the DEL
character (U+007F, 127) in escaped output. This ensures that the
non-printable DEL control character is properly escaped as \u{7f}
instead of being printed directly.
Also add test cases for DEL and other control characters.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
fd0aadfd9a
commit
90e68aaf9c
2 changed files with 37 additions and 1 deletions
|
|
@ -21,6 +21,42 @@ static void tst_ascii_roundtrip() {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Test that control characters are properly escaped.
|
||||||
|
static void tst_control_chars_escaped() {
|
||||||
|
// Test DEL character (0x7F / 127)
|
||||||
|
zstring del_char(0x7Fu);
|
||||||
|
std::string del_encoded = del_char.encode();
|
||||||
|
bool del_ok = del_encoded == "\\u{7f}";
|
||||||
|
|
||||||
|
if (!del_ok) {
|
||||||
|
std::cout << "Failed to escape DEL character (0x7F): got '" << del_encoded
|
||||||
|
<< "', expected '\\u{7f}'\n" << std::flush;
|
||||||
|
ENSURE(del_ok);
|
||||||
|
}
|
||||||
|
|
||||||
|
// Test a few other control characters below 0x20
|
||||||
|
zstring null_char(0x00u);
|
||||||
|
std::string null_encoded = null_char.encode();
|
||||||
|
bool null_ok = null_encoded == "\\u{0}";
|
||||||
|
|
||||||
|
if (!null_ok) {
|
||||||
|
std::cout << "Failed to escape NULL character (0x00): got '" << null_encoded
|
||||||
|
<< "', expected '\\u{0}'\n" << std::flush;
|
||||||
|
ENSURE(null_ok);
|
||||||
|
}
|
||||||
|
|
||||||
|
zstring tab_char(0x09u);
|
||||||
|
std::string tab_encoded = tab_char.encode();
|
||||||
|
bool tab_ok = tab_encoded == "\\u{9}";
|
||||||
|
|
||||||
|
if (!tab_ok) {
|
||||||
|
std::cout << "Failed to escape TAB character (0x09): got '" << tab_encoded
|
||||||
|
<< "', expected '\\u{9}'\n" << std::flush;
|
||||||
|
ENSURE(tab_ok);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
void tst_zstring() {
|
void tst_zstring() {
|
||||||
tst_ascii_roundtrip();
|
tst_ascii_roundtrip();
|
||||||
|
tst_control_chars_escaped();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -150,7 +150,7 @@ std::string zstring::encode() const {
|
||||||
#define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
|
#define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
|
||||||
for (unsigned i = 0; i < m_buffer.size(); ++i) {
|
for (unsigned i = 0; i < m_buffer.size(); ++i) {
|
||||||
unsigned ch = m_buffer[i];
|
unsigned ch = m_buffer[i];
|
||||||
if (ch < 32 || ch >= 128 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) {
|
if (ch < 32 || ch >= 127 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) {
|
||||||
_flush();
|
_flush();
|
||||||
strm << "\\u{" << std::hex << ch << std::dec << '}';
|
strm << "\\u{" << std::hex << ch << std::dec << '}';
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue