mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-31 06:17:55 +00:00
Code Activity

Fix DEL character (0x7F) not being escaped in string literals (#8080)

Browse source 
* Initial plan

* 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>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2025-12-15 22:23:49 +00:00 • committed by GitHub
parent ebe8b5dea5
commit 901a1c3601
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 37 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/zstring.cpp
View file

@ -150,7 +150,7 @@ std::string zstring::encode() const {
#define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
for (unsigned i = 0; i < m_buffer.size(); ++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();
strm << "\\u{" << std::hex << ch << std::dec << '}';
}