mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

string escaping

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-30 04:58:58 -08:00
parent c99b805c14
commit 520b24aab4
3 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.cpp
View file

@ -629,9 +629,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
} }
app* seq_decl_plugin::mk_string(symbol const& s) { app* seq_decl_plugin::mk_string(symbol const& s) {
zstring canonStr(s.bare_str()); parameter param(s);
symbol canonSym(canonStr.encode());
parameter param(canonSym);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param)); func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f); return m_manager->mk_const(f);

3
src/parsers/smt2/smt2parser.cpp
View file

@ -1188,7 +1188,8 @@ namespace smt2 {
void parse_string_const() { void parse_string_const() {
SASSERT(curr() == scanner::STRING_TOKEN); SASSERT(curr() == scanner::STRING_TOKEN);
expr_stack().push_back(sutil().str.mk_string(symbol(m_scanner.get_string()))); zstring zs(m_scanner.get_string());
expr_stack().push_back(sutil().str.mk_string(zs));
TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";); TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
next(); next();
} }

2
src/util/zstring.cpp
View file

@ -137,7 +137,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) { if (ch < 32 || ch >= 128 || ch == '\\') {
_flush(); _flush();
strm << "\\u{" << std::hex << ch << std::dec << "}"; strm << "\\u{" << std::hex << ch << std::dec << "}";
} }