summaryrefslogtreecommitdiff
path: root/Source/Core/Scanner.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/Scanner.cs')
-rw-r--r--Source/Core/Scanner.cs385
1 files changed, 202 insertions, 183 deletions
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index e068fc4b..1185963f 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 96;
- const int noSym = 96;
+ const int maxT = 97;
+ const int noSym = 97;
[ContractInvariantMethod]
@@ -267,41 +267,41 @@ public class Scanner {
for (int i = 65; i <= 90; ++i) start[i] = 2;
for (int i = 94; i <= 122; ++i) start[i] = 2;
for (int i = 126; i <= 126; ++i) start[i] = 2;
- for (int i = 48; i <= 57; ++i) start[i] = 16;
+ for (int i = 48; i <= 57; ++i) start[i] = 19;
for (int i = 34; i <= 34; ++i) start[i] = 6;
start[92] = 1;
- start[59] = 19;
- start[40] = 20;
- start[41] = 21;
- start[58] = 55;
- start[44] = 22;
- start[91] = 23;
- start[93] = 24;
- start[60] = 56;
- start[62] = 57;
- start[123] = 25;
- start[125] = 58;
- start[61] = 59;
- start[42] = 60;
- start[124] = 61;
- start[8660] = 28;
- start[8658] = 30;
- start[8656] = 31;
- start[38] = 32;
- start[8743] = 34;
- start[8744] = 36;
- start[33] = 62;
- start[8800] = 40;
- start[8804] = 41;
- start[8805] = 42;
- start[43] = 63;
- start[45] = 44;
- start[47] = 45;
- start[172] = 47;
- start[8704] = 50;
- start[8707] = 51;
- start[955] = 52;
- start[8226] = 54;
+ start[59] = 24;
+ start[40] = 25;
+ start[41] = 26;
+ start[58] = 60;
+ start[44] = 27;
+ start[91] = 28;
+ start[93] = 29;
+ start[60] = 61;
+ start[62] = 62;
+ start[123] = 30;
+ start[125] = 63;
+ start[61] = 64;
+ start[42] = 65;
+ start[124] = 66;
+ start[8660] = 33;
+ start[8658] = 35;
+ start[8656] = 36;
+ start[38] = 37;
+ start[8743] = 39;
+ start[8744] = 41;
+ start[33] = 67;
+ start[8800] = 45;
+ start[8804] = 46;
+ start[8805] = 47;
+ start[43] = 68;
+ start[45] = 49;
+ start[47] = 50;
+ start[172] = 52;
+ start[8704] = 55;
+ start[8707] = 56;
+ start[955] = 57;
+ start[8226] = 59;
start[Buffer.EOF] = -1;
}
@@ -503,48 +503,48 @@ public class Scanner {
void CheckLiteral() {
switch (t.val) {
- case "var": t.kind = 7; break;
- case "where": t.kind = 13; break;
- case "int": t.kind = 14; break;
- case "real": t.kind = 15; break;
- case "bool": t.kind = 16; break;
- case "const": t.kind = 21; break;
- case "unique": t.kind = 22; break;
- case "extends": t.kind = 23; break;
- case "complete": t.kind = 24; break;
- case "function": t.kind = 25; break;
- case "returns": t.kind = 26; break;
- case "axiom": t.kind = 29; break;
- case "type": t.kind = 30; break;
- case "procedure": t.kind = 32; break;
- case "implementation": t.kind = 33; break;
- case "modifies": t.kind = 34; break;
- case "free": t.kind = 35; break;
- case "requires": t.kind = 36; break;
- case "ensures": t.kind = 37; break;
- case "goto": t.kind = 38; break;
- case "return": t.kind = 39; break;
- case "if": t.kind = 40; break;
- case "else": t.kind = 41; break;
- case "while": t.kind = 42; break;
- case "invariant": t.kind = 43; break;
- case "break": t.kind = 45; break;
- case "assert": t.kind = 46; break;
- case "assume": t.kind = 47; break;
- case "havoc": t.kind = 48; break;
- case "yield": t.kind = 49; break;
- case "async": t.kind = 51; break;
- case "call": t.kind = 52; break;
- case "par": t.kind = 53; break;
- case "div": t.kind = 76; break;
- case "mod": t.kind = 77; break;
- case "false": t.kind = 82; break;
- case "true": t.kind = 83; break;
- case "old": t.kind = 84; break;
- case "then": t.kind = 87; break;
- case "forall": t.kind = 88; break;
- case "exists": t.kind = 90; break;
- case "lambda": t.kind = 92; break;
+ case "var": t.kind = 8; break;
+ case "where": t.kind = 14; break;
+ case "int": t.kind = 15; break;
+ case "real": t.kind = 16; break;
+ case "bool": t.kind = 17; break;
+ case "const": t.kind = 22; break;
+ case "unique": t.kind = 23; break;
+ case "extends": t.kind = 24; break;
+ case "complete": t.kind = 25; break;
+ case "function": t.kind = 26; break;
+ case "returns": t.kind = 27; break;
+ case "axiom": t.kind = 30; break;
+ case "type": t.kind = 31; break;
+ case "procedure": t.kind = 33; break;
+ case "implementation": t.kind = 34; break;
+ case "modifies": t.kind = 35; break;
+ case "free": t.kind = 36; break;
+ case "requires": t.kind = 37; break;
+ case "ensures": t.kind = 38; break;
+ case "goto": t.kind = 39; break;
+ case "return": t.kind = 40; break;
+ case "if": t.kind = 41; break;
+ case "else": t.kind = 42; break;
+ case "while": t.kind = 43; break;
+ case "invariant": t.kind = 44; break;
+ case "break": t.kind = 46; break;
+ case "assert": t.kind = 47; break;
+ case "assume": t.kind = 48; break;
+ case "havoc": t.kind = 49; break;
+ case "yield": t.kind = 50; break;
+ case "async": t.kind = 52; break;
+ case "call": t.kind = 53; break;
+ case "par": t.kind = 54; break;
+ case "div": t.kind = 77; break;
+ case "mod": t.kind = 78; break;
+ case "false": t.kind = 83; break;
+ case "true": t.kind = 84; break;
+ case "old": t.kind = 85; break;
+ case "then": t.kind = 88; break;
+ case "forall": t.kind = 89; break;
+ case "exists": t.kind = 91; break;
+ case "lambda": t.kind = 93; break;
default: break;
}
}
@@ -597,182 +597,201 @@ public class Scanner {
case 6:
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 20;}
else {goto case 0;}
case 7:
{t.kind = 4; break;}
case 8:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else if (ch == '-') {AddCh(); goto case 9;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
else {goto case 0;}
case 9:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else {goto case 0;}
- case 10:
recEnd = pos; recKind = 5;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
else {t.kind = 5; break;}
- case 11:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ case 10:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
else {goto case 0;}
- case 12:
+ case 11:
recEnd = pos; recKind = 6;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
- else if (ch == 'e') {AddCh(); goto case 13;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
+ else if (ch == 'e') {AddCh(); goto case 12;}
else {t.kind = 6; break;}
+ case 12:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
+ else if (ch == '-') {AddCh(); goto case 13;}
+ else {goto case 0;}
case 13:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else if (ch == '-') {AddCh(); goto case 14;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
else {goto case 0;}
case 14:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else {goto case 0;}
- case 15:
recEnd = pos; recKind = 6;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
else {t.kind = 6; break;}
+ case 15:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else {goto case 0;}
case 16:
- recEnd = pos; recKind = 3;
if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else if (ch == 'e') {AddCh(); goto case 17;}
+ else {goto case 0;}
+ case 17:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+ else {goto case 0;}
+ case 18:
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+ else {t.kind = 7; break;}
+ case 19:
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;}
else if (ch == 'b') {AddCh(); goto case 3;}
- else if (ch == 'e') {AddCh(); goto case 8;}
- else if (ch == '.') {AddCh(); goto case 11;}
+ else if (ch == 'e') {AddCh(); goto case 21;}
+ else if (ch == '.') {AddCh(); goto case 10;}
else {t.kind = 3; break;}
- case 17:
- if (ch == '"') {AddCh(); goto case 18;}
+ case 20:
+ if (ch == '"') {AddCh(); goto case 22;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 20;}
else {goto case 0;}
- case 18:
+ case 21:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
+ else if (ch == '-') {AddCh(); goto case 8;}
+ else {goto case 0;}
+ case 22:
recEnd = pos; recKind = 4;
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 20;}
else {t.kind = 4; break;}
- case 19:
- {t.kind = 8; break;}
- case 20:
- {t.kind = 9; break;}
- case 21:
- {t.kind = 10; break;}
- case 22:
- {t.kind = 12; break;}
case 23:
- {t.kind = 17; break;}
+ recEnd = pos; recKind = 5;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
+ else if (ch == 'f') {AddCh(); goto case 15;}
+ else {t.kind = 5; break;}
case 24:
- {t.kind = 18; break;}
+ {t.kind = 9; break;}
case 25:
- {t.kind = 27; break;}
+ {t.kind = 10; break;}
case 26:
- {t.kind = 50; break;}
+ {t.kind = 11; break;}
case 27:
- {t.kind = 55; break;}
+ {t.kind = 13; break;}
case 28:
- {t.kind = 56; break;}
+ {t.kind = 18; break;}
case 29:
- {t.kind = 57; break;}
+ {t.kind = 19; break;}
case 30:
- {t.kind = 58; break;}
+ {t.kind = 28; break;}
case 31:
- {t.kind = 60; break;}
+ {t.kind = 51; break;}
case 32:
- if (ch == '&') {AddCh(); goto case 33;}
- else {goto case 0;}
+ {t.kind = 56; break;}
case 33:
- {t.kind = 61; break;}
+ {t.kind = 57; break;}
case 34:
- {t.kind = 62; break;}
+ {t.kind = 58; break;}
case 35:
- {t.kind = 63; break;}
+ {t.kind = 59; break;}
case 36:
- {t.kind = 64; break;}
+ {t.kind = 61; break;}
case 37:
- {t.kind = 67; break;}
+ if (ch == '&') {AddCh(); goto case 38;}
+ else {goto case 0;}
case 38:
- {t.kind = 68; break;}
+ {t.kind = 62; break;}
case 39:
- {t.kind = 69; break;}
+ {t.kind = 63; break;}
case 40:
- {t.kind = 70; break;}
+ {t.kind = 64; break;}
case 41:
- {t.kind = 71; break;}
+ {t.kind = 65; break;}
case 42:
- {t.kind = 72; break;}
+ {t.kind = 68; break;}
case 43:
- {t.kind = 73; break;}
+ {t.kind = 69; break;}
case 44:
- {t.kind = 75; break;}
+ {t.kind = 70; break;}
case 45:
- {t.kind = 78; break;}
+ {t.kind = 71; break;}
case 46:
- {t.kind = 79; break;}
+ {t.kind = 72; break;}
case 47:
- {t.kind = 81; break;}
+ {t.kind = 73; break;}
case 48:
- {t.kind = 85; break;}
+ {t.kind = 74; break;}
case 49:
- {t.kind = 86; break;}
+ {t.kind = 76; break;}
case 50:
- {t.kind = 89; break;}
+ {t.kind = 79; break;}
case 51:
- {t.kind = 91; break;}
+ {t.kind = 80; break;}
case 52:
- {t.kind = 93; break;}
+ {t.kind = 82; break;}
case 53:
- {t.kind = 94; break;}
+ {t.kind = 86; break;}
case 54:
- {t.kind = 95; break;}
+ {t.kind = 87; break;}
case 55:
- recEnd = pos; recKind = 11;
- if (ch == '=') {AddCh(); goto case 26;}
- else if (ch == ':') {AddCh(); goto case 53;}
- else {t.kind = 11; break;}
+ {t.kind = 90; break;}
case 56:
- recEnd = pos; recKind = 19;
- if (ch == '=') {AddCh(); goto case 64;}
- else if (ch == ':') {AddCh(); goto case 39;}
- else {t.kind = 19; break;}
+ {t.kind = 92; break;}
case 57:
- recEnd = pos; recKind = 20;
- if (ch == '=') {AddCh(); goto case 37;}
- else {t.kind = 20; break;}
+ {t.kind = 94; break;}
case 58:
- recEnd = pos; recKind = 28;
- if (ch == '|') {AddCh(); goto case 49;}
- else {t.kind = 28; break;}
+ {t.kind = 95; break;}
case 59:
- recEnd = pos; recKind = 31;
- if (ch == '=') {AddCh(); goto case 65;}
- else {t.kind = 31; break;}
+ {t.kind = 96; break;}
case 60:
- recEnd = pos; recKind = 44;
- if (ch == '*') {AddCh(); goto case 46;}
- else {t.kind = 44; break;}
+ recEnd = pos; recKind = 12;
+ if (ch == '=') {AddCh(); goto case 31;}
+ else if (ch == ':') {AddCh(); goto case 58;}
+ else {t.kind = 12; break;}
case 61:
- recEnd = pos; recKind = 54;
- if (ch == '|') {AddCh(); goto case 35;}
- else if (ch == '{') {AddCh(); goto case 48;}
- else {t.kind = 54; break;}
+ recEnd = pos; recKind = 20;
+ if (ch == '=') {AddCh(); goto case 69;}
+ else if (ch == ':') {AddCh(); goto case 44;}
+ else {t.kind = 20; break;}
case 62:
- recEnd = pos; recKind = 80;
- if (ch == '=') {AddCh(); goto case 38;}
- else {t.kind = 80; break;}
+ recEnd = pos; recKind = 21;
+ if (ch == '=') {AddCh(); goto case 42;}
+ else {t.kind = 21; break;}
case 63:
- recEnd = pos; recKind = 74;
- if (ch == '+') {AddCh(); goto case 43;}
- else {t.kind = 74; break;}
+ recEnd = pos; recKind = 29;
+ if (ch == '|') {AddCh(); goto case 54;}
+ else {t.kind = 29; break;}
case 64:
- recEnd = pos; recKind = 66;
- if (ch == '=') {AddCh(); goto case 66;}
- else {t.kind = 66; break;}
+ recEnd = pos; recKind = 32;
+ if (ch == '=') {AddCh(); goto case 70;}
+ else {t.kind = 32; break;}
case 65:
- recEnd = pos; recKind = 65;
- if (ch == '>') {AddCh(); goto case 29;}
- else {t.kind = 65; break;}
+ recEnd = pos; recKind = 45;
+ if (ch == '*') {AddCh(); goto case 51;}
+ else {t.kind = 45; break;}
case 66:
- recEnd = pos; recKind = 59;
- if (ch == '>') {AddCh(); goto case 27;}
- else {t.kind = 59; break;}
+ recEnd = pos; recKind = 55;
+ if (ch == '|') {AddCh(); goto case 40;}
+ else if (ch == '{') {AddCh(); goto case 53;}
+ else {t.kind = 55; break;}
+ case 67:
+ recEnd = pos; recKind = 81;
+ if (ch == '=') {AddCh(); goto case 43;}
+ else {t.kind = 81; break;}
+ case 68:
+ recEnd = pos; recKind = 75;
+ if (ch == '+') {AddCh(); goto case 48;}
+ else {t.kind = 75; break;}
+ case 69:
+ recEnd = pos; recKind = 67;
+ if (ch == '=') {AddCh(); goto case 71;}
+ else {t.kind = 67; break;}
+ case 70:
+ recEnd = pos; recKind = 66;
+ if (ch == '>') {AddCh(); goto case 34;}
+ else {t.kind = 66; break;}
+ case 71:
+ recEnd = pos; recKind = 60;
+ if (ch == '>') {AddCh(); goto case 32;}
+ else {t.kind = 60; break;}
}
t.val = new String(tval, 0, tlen);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 00:19:09 +0000