mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 22:20:54 +00:00
Code Activity

escape chars in smt2 printing of string constants

Browse source
This commit is contained in:
Murphy Berzish 2016-11-22 18:32:03 -05:00
parent 11d8ffc4d4
commit 8e962aa427
2 changed files with 40 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/ast/ast_smt2_pp.cpp
View file

@ -305,14 +305,45 @@ format * smt2_pp_environment::mk_float(rational const & val) const {
}
format * smt2_pp_environment::pp_str_literal(app * t) {
TRACE("parse_string", tout << "pp_str_literal\n";);
str_util & u = get_strutil();
SASSERT(u.is_string(t));
const char * val;
u.is_string(t, &val);
ast_manager & m = get_manager();
str_util & u = get_strutil();
TRACE("parse_string", tout << "pp_str_literal\n";);
SASSERT(u.is_string(t));
std::string strVal = u.get_string_constant_value(t);
string_buffer<> buf;
buf << "\"" << val << "\"";
buf << "\"";
// we want to scan strVal and escape every non-printable character
for (unsigned int i = 0; i < strVal.length(); ++i) {
char c = strVal.at(i);
if (isprint(c)) {
buf << c;
} else if (c == '\a') {
buf << "\\a";
} else if (c == '\b') {
buf << "\\b";
} else if (c == '\e') {
buf << "\\e";
} else if (c == '\f') {
buf << "\\f";
} else if (c == '\n') {
buf << "\\n";
} else if (c == '\r') {
buf << "\\r";
} else if (c == '\t') {
buf << "\\t";
} else if (c == '\v') {
buf << "\\v";
} else if (c == '\\') {
buf << "\\" << "\\";
} else {
// TODO general hex escape
NOT_IMPLEMENTED_YET();
}
}
buf << "\"";
return mk_string(m, buf.c_str());
}