diff options
author | boehmes <unknown> | 2012-09-27 17:13:42 +0200 |
---|---|---|
committer | boehmes <unknown> | 2012-09-27 17:13:42 +0200 |
commit | 623a87c132abec61b5c74a6a00a7b162073a6a8d (patch) | |
tree | b95ba791592cf395ce99035715de98578a5519ee /Source/Core | |
parent | ed83becd12d7079e6ce2853fbebace20b1e7df5a (diff) |
Boogie: new syntax for integer division and modulus: use div and mod instead of / and %
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/AbsyExpr.cs | 4 | ||||
-rw-r--r-- | Source/Core/BoogiePL.atg | 4 | ||||
-rw-r--r-- | Source/Core/Parser.cs | 4 | ||||
-rw-r--r-- | Source/Core/Scanner.cs | 82 | ||||
-rw-r--r-- | Source/Core/Util.cs | 4 |
5 files changed, 47 insertions, 51 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index f2ed5790..d2b8506a 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1214,9 +1214,9 @@ namespace Microsoft.Boogie { case Opcode.Mul:
return "*";
case Opcode.Div:
- return "/";
+ return "div";
case Opcode.Mod:
- return "%";
+ return "mod";
case Opcode.Eq:
return "==";
case Opcode.Neq:
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index a2ad40f6..26b70bd3 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1171,8 +1171,8 @@ Factor<out Expr/*!*/ e0> MulOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .)
- | "/" (. x = t; op=BinaryOperator.Opcode.Div; .)
- | "%" (. x = t; op=BinaryOperator.Opcode.Mod; .)
+ | "div" (. x = t; op=BinaryOperator.Opcode.Div; .)
+ | "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .)
)
.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index e95bccda..8638d9c3 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -2157,8 +2157,8 @@ public class Errors { case 68: s = "\"++\" expected"; break;
case 69: s = "\"+\" expected"; break;
case 70: s = "\"-\" expected"; break;
- case 71: s = "\"/\" expected"; break;
- case 72: s = "\"%\" expected"; break;
+ case 71: s = "\"div\" expected"; break;
+ case 72: s = "\"mod\" expected"; break;
case 73: s = "\"!\" expected"; break;
case 74: s = "\"\\u00ac\" expected"; break;
case 75: s = "\"false\" expected"; break;
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index cfef86c7..b9f4ec42 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -262,36 +262,34 @@ public class Scanner { start[59] = 12;
start[40] = 13;
start[41] = 14;
- start[58] = 49;
+ start[58] = 47;
start[44] = 15;
start[91] = 16;
start[93] = 17;
- start[60] = 50;
- start[62] = 51;
+ start[60] = 48;
+ start[62] = 49;
start[123] = 18;
- start[125] = 52;
- start[61] = 53;
+ start[125] = 50;
+ start[61] = 51;
start[42] = 19;
start[8660] = 22;
start[8658] = 24;
start[8656] = 25;
start[38] = 26;
start[8743] = 28;
- start[124] = 54;
+ start[124] = 52;
start[8744] = 30;
- start[33] = 55;
+ start[33] = 53;
start[8800] = 34;
start[8804] = 35;
start[8805] = 36;
- start[43] = 56;
+ start[43] = 54;
start[45] = 38;
- start[47] = 39;
- start[37] = 40;
- start[172] = 41;
- start[8704] = 44;
- start[8707] = 45;
- start[955] = 46;
- start[8226] = 48;
+ start[172] = 39;
+ start[8704] = 42;
+ start[8707] = 43;
+ start[955] = 44;
+ start[8226] = 46;
start[Buffer.EOF] = -1;
}
@@ -519,6 +517,8 @@ public class Scanner { case "havoc": t.kind = 46; break;
case "call": t.kind = 48; break;
case "forall": t.kind = 49; break;
+ case "div": t.kind = 71; break;
+ case "mod": t.kind = 72; break;
case "false": t.kind = 75; break;
case "true": t.kind = 76; break;
case "old": t.kind = 77; break;
@@ -658,68 +658,64 @@ public class Scanner { case 38:
{t.kind = 70; break;}
case 39:
- {t.kind = 71; break;}
- case 40:
- {t.kind = 72; break;}
- case 41:
{t.kind = 74; break;}
- case 42:
+ case 40:
{t.kind = 78; break;}
- case 43:
+ case 41:
{t.kind = 79; break;}
- case 44:
+ case 42:
{t.kind = 81; break;}
- case 45:
+ case 43:
{t.kind = 83; break;}
- case 46:
+ case 44:
{t.kind = 85; break;}
- case 47:
+ case 45:
{t.kind = 86; break;}
- case 48:
+ case 46:
{t.kind = 87; break;}
- case 49:
+ case 47:
recEnd = pos; recKind = 10;
if (ch == '=') {AddCh(); goto case 20;}
- else if (ch == ':') {AddCh(); goto case 47;}
+ else if (ch == ':') {AddCh(); goto case 45;}
else {t.kind = 10; break;}
- case 50:
+ case 48:
recEnd = pos; recKind = 17;
- if (ch == '=') {AddCh(); goto case 57;}
+ if (ch == '=') {AddCh(); goto case 55;}
else if (ch == ':') {AddCh(); goto case 33;}
else {t.kind = 17; break;}
- case 51:
+ case 49:
recEnd = pos; recKind = 18;
if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 18; break;}
- case 52:
+ case 50:
recEnd = pos; recKind = 26;
- if (ch == '|') {AddCh(); goto case 43;}
+ if (ch == '|') {AddCh(); goto case 41;}
else {t.kind = 26; break;}
- case 53:
+ case 51:
recEnd = pos; recKind = 29;
- if (ch == '=') {AddCh(); goto case 58;}
+ if (ch == '=') {AddCh(); goto case 56;}
else {t.kind = 29; break;}
- case 54:
+ case 52:
if (ch == '|') {AddCh(); goto case 29;}
- else if (ch == '{') {AddCh(); goto case 42;}
+ else if (ch == '{') {AddCh(); goto case 40;}
else {goto case 0;}
- case 55:
+ case 53:
recEnd = pos; recKind = 73;
if (ch == '=') {AddCh(); goto case 32;}
else {t.kind = 73; break;}
- case 56:
+ case 54:
recEnd = pos; recKind = 69;
if (ch == '+') {AddCh(); goto case 37;}
else {t.kind = 69; break;}
- case 57:
+ case 55:
recEnd = pos; recKind = 61;
- if (ch == '=') {AddCh(); goto case 59;}
+ if (ch == '=') {AddCh(); goto case 57;}
else {t.kind = 61; break;}
- case 58:
+ case 56:
recEnd = pos; recKind = 60;
if (ch == '>') {AddCh(); goto case 23;}
else {t.kind = 60; break;}
- case 59:
+ case 57:
recEnd = pos; recKind = 54;
if (ch == '>') {AddCh(); goto case 21;}
else {t.kind = 54; break;}
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index a8e12f63..f8b8b82b 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -451,7 +451,7 @@ namespace Microsoft.Boogie { op = " && ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Div:
- op = " / ";
+ op = " div ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Eq:
op = " == ";
@@ -475,7 +475,7 @@ namespace Microsoft.Boogie { op = " < ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Mod:
- op = " % ";
+ op = " mod ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Mul:
op = " * ";
|