Reject un-escaped extended ASCII characters

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 441af0308664f2cd7d0a96f7188d7d44f8281aa6..3f0bc46fd06c3bcf7c6ec6fc8a08c642567440b1 100644 (file)
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -41,15 +41,14 @@ void String::toInternal(const std::string &s) {
           case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;\r
           case 'x': {\r
             if(i + 2 < s.size()) {\r
-            if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] <= 'f') || (s[i+1] >= 'A' && s[i+1] <= 'F')) &&\r
-               (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] <= 'f') || (s[i+2] >= 'A' && s[i+2] <= 'F'))) {\r
-              d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );\r
-              i += 3;\r
-            } else {\r
-              throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );\r
-            }\r
+              if(isxdigit(s[i+1]) && isxdigit(s[i+2])) {\r
+                d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );\r
+                i += 3;\r
+              } else {\r
+                throw CVC4::Exception( "Illegal String Literal: \"" + s + "\"" );\r
+              }\r
             } else {\r
-            throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );\r
+              throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must have two digits after \\x" );\r
             }\r
           }\r
           break;\r
@@ -71,6 +70,8 @@ void String::toInternal(const std::string &s) {
                 d_str.push_back( convertCharToUnsignedInt((char)num) );\r
                 i++;\r
               }\r
+            } else if((unsigned)s[i] > 127) {\r
+              throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" );\r
             } else {\r
               d_str.push_back( convertCharToUnsignedInt(s[i]) );\r
               i++;\r
@@ -81,6 +82,8 @@ void String::toInternal(const std::string &s) {
         throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );\r
         //d_str.push_back( convertCharToUnsignedInt('\\') );\r
       }\r
+    } else if((unsigned)s[i] > 127) {\r
+      throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" );\r
     } else {\r
       d_str.push_back( convertCharToUnsignedInt(s[i]) );\r
       i++;\r