From 2d0ba1036e35a6ce6cb8d5cd9e68d311ae8cde80 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 9 Jan 2015 09:40:10 -0600 Subject: [PATCH] blocked unprintable characters in string literals; disabled string literal test case for smtlib v2.5 --- src/parser/smt2/Smt2.g | 8 ++++---- src/printer/smt2/smt2_printer.cpp | 6 +++--- test/regress/regress0/parser/Makefile.am | 5 +++-- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1a5442419..22b2244a0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1540,8 +1540,8 @@ str[std::string& s, bool fsmtlib] /* strip off the quotes */ s = s.substr(1, s.size() - 2); for(size_t i=0; i 127) { - PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); + if((unsigned)s[i] > 127 && !isprint(s[i])) { + PARSER_STATE->parseError("Extended/unprintable characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); } } if(fsmtlib) { @@ -1572,8 +1572,8 @@ str[std::string& s, bool fsmtlib] /* strip off the quotes */ s = s.substr(1, s.size() - 2); for(size_t i=0; i 127) { - PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); + if((unsigned)s[i] > 127 && !isprint(s[i])) { + PARSER_STATE->parseError("Extended/unprintable characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); } } // In the 2.5 version, always handle escapes (regardless of fsmtlib flag). diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 72a64ab78..e72de92fd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -223,13 +223,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, char c = s[i]; if(c == '"') { if(d_variant == z3str_variant || d_variant == smt2_0_variant) { - out << "\\\""; + out << c; //out << "\\\""; } else { out << "\"\""; } - } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) { + } /*else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) { out << "\\\\"; - } else { + }*/ else { out << c; } } diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am index eb27e797b..3808bd54d 100644 --- a/test/regress/regress0/parser/Makefile.am +++ b/test/regress/regress0/parser/Makefile.am @@ -20,8 +20,9 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ declarefun-emptyset-uf.smt2 \ - strings20.smt2 \ - strings25.smt2 + strings20.smt2 + +# strings25.smt2 EXTRA_DIST = $(TESTS) -- 2.30.2