mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

patch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-22 12:26:54 -07:00
parent e14e3ef291
commit 5cb0bac41d
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/zstring.cpp
View file

@ -33,7 +33,7 @@ static bool is_hex_digit(char ch, unsigned& d) {
return false;
}
bool zstring::is_escape_char(char const *& s, unsigned& result) {
bool zstring::is_escape_char(bool from_input, char const *& s, unsigned& result) {
unsigned d;
if (*s == '\\' && s[1] == 'u' && s[2] == '{' && s[3] != '}') {
result = 0;
@ -55,6 +55,8 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) {
}
return false;
}
if (!from_input)
return false;
unsigned d1, d2, d3, d4;
if (*s == '\\' && s[1] == 'u' &&
is_hex_digit(s[2], d1) &&
@ -76,7 +78,7 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) {
zstring::zstring(char const* s, bool from_input) {
while (*s) {
unsigned ch = 0;
if (from_input && is_escape_char(s, ch)) {
if (is_escape_char(from_input, s, ch)) {
m_buffer.push_back(ch);
}
else {

2
src/util/zstring.h
View file

@ -25,7 +25,7 @@ private:
buffer<unsigned> m_buffer;
bool well_formed() const;
bool uses_unicode() const;
bool is_escape_char(char const *& s, unsigned& result);
bool is_escape_char(bool from_input, char const *& s, unsigned& result);
public:
static unsigned unicode_max_char() { return 196607; }
static unsigned unicode_num_bits() { return 18; }