diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-10 21:04:58 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-25 15:02:33 -0500 |
commit | 1b916866274cc238c708f25fbb8c17add33d3376 (patch) | |
tree | ab48fb94dfe76aeeff46fe1e71e69e350207d4d8 /src | |
parent | d9ffaf6ed5d2de15d1982b423be6fa6d5f9d8995 (diff) |
Fix quotes in string constants.
Diffstat (limited to 'src')
-rw-r--r-- | src/util/regexp.h | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/util/regexp.h b/src/util/regexp.h index 46417cdb6..0cd92810b 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -21,6 +21,7 @@ #define __CVC4__REGEXP_H #include <iostream> +#include <iomanip> #include <string> #include <sstream> #include "util/exception.h" @@ -390,7 +391,18 @@ struct CVC4_PUBLIC StringHashFunction { inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const String& s) { - return os << "\"" << s.toString() << "\""; + os << '"'; + std::string str = s.toString(); + for(std::string::iterator i = str.begin(); i != str.end(); ++i) { + if(*i == '\\' || *i == '"') { + os << '\\'; + } else if(!isprint(*i)) { + os << "\\x" << std::ios::hex << std::setw(2) << (unsigned(*i) % 0x100); + continue; + } + os << *i; + } + return os << '"'; } class CVC4_PUBLIC RegExp { |