mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-02-24 07:54:25 -08:00
parent b0dd3f3238 e744d0f271
commit 8437cb7132
1 changed files with 32 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/ast/seq_decl_plugin.cpp
View file

@ -38,8 +38,16 @@ static bool is_hex_digit(char ch, unsigned& d) {
return false;
}
static bool is_octal_digit(char ch, unsigned& d) {
if ('0' <= ch && ch <= '7') {
d = ch - '0';
return true;
}
return false;
}
static bool is_escape_char(char const *& s, unsigned& result) {
unsigned d1, d2;
unsigned d1, d2, d3;
if (*s != '\\' || *(s + 1) == 0) {
return false;
}
@ -49,6 +57,29 @@ static bool is_escape_char(char const *& s, unsigned& result) {
s += 4;
return true;
}
/* C-standard octal escapes: either 1, 2, or 3 octal digits,
* stopping either at 3 digits or at the first non-digit character.
*/
/* 1 octal digit */
if (is_octal_digit(*(s + 1), d1) && !is_octal_digit(*(s + 2), d2)) {
result = d1;
s += 2;
return true;
}
/* 2 octal digits */
if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) &&
!is_octal_digit(*(s + 3), d3)) {
result = d1 * 8 + d2;
s += 3;
return true;
}
/* 3 octal digits */
if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) &&
is_octal_digit(*(s + 3), d3)) {
result = d1*64 + d2*8 + d3;
s += 4;
return true;
}
switch (*(s + 1)) {
case 'a':
result = '\a';